		Search-engine friendly clone of the ACL2 documentation.

Expdata-event-generation

Expdata-gen-result-vars-aux

Signature
(expdata-gen-result-vars-aux old$ j m) → vars
Arguments: old$ — Guard (symbolp old$).; j — Guard (posp j).; m — Guard (posp m).
Returns: vars — Type (symbol-listp vars).

Definitions and Theorems

Function: expdata-gen-result-vars-aux

(defun expdata-gen-result-vars-aux (old$ j m)
  (declare (xargs :guard (and (symbolp old$) (posp j) (posp m))))
  (let ((__function__ 'expdata-gen-result-vars-aux))
    (declare (ignorable __function__))
    (b* (((unless (mbt (posp j))) nil)
         ((unless (mbt (posp m))) nil)
         ((when (> j m)) nil)
         (name (str::cat "RESULT" (str::nat-to-dec-string j)))
         (var (intern-in-package-of-symbol name old$))
         (vars (expdata-gen-result-vars-aux old$ (1+ j)
                                            m)))
      (cons var vars))))

Theorem: symbol-listp-of-expdata-gen-result-vars-aux

(defthm symbol-listp-of-expdata-gen-result-vars-aux
  (b* ((vars (expdata-gen-result-vars-aux old$ j m)))
    (symbol-listp vars))
  :rule-classes :rewrite)