		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-constraint

Shallowly embedded semantics of a constraint.

Signature
(lift-constraint constr prime state) → term
Arguments: constr — Guard (constraintp constr).; prime — Guard (symbolp prime).

We turn an equality constraint into an ACL2 equality of the terms denoted by the left and right expressions. We turn a relation constraint into an ACL2 call of the relation on the terms denoted by the argument expressions. Note that we include the variable for the prime.

Definitions and Theorems

Function: lift-constraint

(defun lift-constraint (constr prime state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (constraintp constr)
                             (symbolp prime))))
 (let ((__function__ 'lift-constraint))
   (declare (ignorable __function__))
   (constraint-case
        constr
        :equal
        (cons 'equal
              (cons (lift-expression constr.left prime state)
                    (cons (lift-expression constr.right prime state)
                          'nil)))
        :relation
        (cons (lift-rel-name constr.name (w state))
              (append (lift-expression-list constr.args prime state)
                      (cons prime 'nil))))))