		Search-engine friendly clone of the ACL2 documentation.

Defequal-input-processing

Defequal-process-vars-aux

Signature
(defequal-process-vars-aux name n) → x1...xn
Arguments: name — Guard (symbolp name).; n — Guard (natp n).
Returns: x1...xn — Type (symbol-listp x1...xn).

Definitions and Theorems

Function: defequal-process-vars-aux

(defun defequal-process-vars-aux (name n)
  (declare (xargs :guard (and (symbolp name) (natp n))))
  (let ((__function__ 'defequal-process-vars-aux))
    (declare (ignorable __function__))
    (cond ((zp n) nil)
          (t (append (defequal-process-vars-aux name (1- n))
                     (list (packn-pos (list "X" n) name)))))))

Theorem: symbol-listp-of-defequal-process-vars-aux

(defthm symbol-listp-of-defequal-process-vars-aux
  (b* ((x1...xn (defequal-process-vars-aux name n)))
    (symbol-listp x1...xn))
  :rule-classes :rewrite)