• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
      • Soft-future-work
      • Soft-macros
        • Defun-inst
        • Defequal
          • Defequal-implementation
            • Defequal-fn
            • Defequal-event-generation
            • Defequal-input-processing
              • Defequal-process-inputs
              • Defequal-process-left-and-right
              • Defequal-process-vars
              • Defequal-process-right-to-left-name
              • Defequal-process-left-to-right-name
              • Defequal-process-vars-aux
              • Defequal-process-name
            • Defequal-table
            • Defequal-macro-definition
        • Defsoft
        • Defthm-inst
        • Defun2
        • Defunvar
        • Defun-sk2
        • Defchoose2
        • Defthm-2nd-order
        • Define-sk2
        • Defund-sk2
        • Define2
        • Defund2
      • Updates-to-workshop-material
      • Soft-implementation
      • Soft-notions
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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)