		Search-engine friendly clone of the ACL2 documentation.

Parteval-event-generation

Parteval-gen-static-equalities

Generate the equalities whose conjunction forms the antecedent of the theorem relating old and new function.

Signature
(parteval-gen-static-equalities static$) → equalities
Arguments: static$ — Guard (symbol-alistp static$).
Returns: equalities — A pseudo-term-listp.

Each equality has the form (equal yj cj).

Definitions and Theorems

Function: parteval-gen-static-equalities

(defun parteval-gen-static-equalities (static$)
  (declare (xargs :guard (symbol-alistp static$)))
  (let ((__function__ 'parteval-gen-static-equalities))
    (declare (ignorable __function__))
    (b* (((when (endp static$)) nil)
         ((cons arg$ static$) static$)
         (equality (cons 'equal
                         (cons (car arg$)
                               (cons (cdr arg$) 'nil))))
         (equalities (parteval-gen-static-equalities static$)))
      (cons equality equalities))))