		Search-engine friendly clone of the ACL2 documentation.

Defequal-input-processing

Defequal-process-vars

Process the :vars input.

Signature
(defequal-process-vars vars name left right n ctx state) → (mv erp x1...xn state)
Arguments: name — Guard (symbolp name).; left — Guard (symbolp left).; right — Guard (symbolp right).; 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)

Function: defequal-process-vars

(defun defequal-process-vars (vars name left right n ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp name)
                             (symbolp left)
                             (symbolp right)
                             (natp n))))
 (let ((__function__ 'defequal-process-vars))
  (declare (ignorable __function__))
  (if (eq vars :auto)
      (value (defequal-process-vars-aux name n))
   (b*
    (((er &)
      (ensure-value-is-symbol-list$ vars "The :VARS input" t nil))
     ((er &)
      (ensure-list-has-no-duplicates$
       vars
       (msg "The list ~x0 of variables specified by the :VARS input"
            vars)
       t nil))
     ((unless (= (len vars) n))
      (er-soft+
       ctx t nil
       "The number of variables ~x0 specified by the :VARS input ~
                     must be equal to the arity ~x1 ~
                     of the functions ~x2 and ~x3 ~
                     specified by the :LEFT and :RIGHT inputs, ~
                     but it is ~x4 instead."
       vars n left right (len vars))))
    (value vars)))))

Theorem: symbol-listp-of-defequal-process-vars.x1...xn

(defthm symbol-listp-of-defequal-process-vars.x1...xn
  (b* (((mv ?erp ?x1...xn acl2::?state)
        (defequal-process-vars vars name left right n ctx state)))
    (symbol-listp x1...xn))
  :rule-classes :rewrite)