		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-constraint-list

Shallowly embedded semantics of a list of constraints.

Signature
(lift-constraint-list constrs prime state) → terms
Arguments: constrs — Guard (constraint-listp constrs).; prime — Guard (symbolp prime).
Returns: terms — Type (true-listp terms).

This lifts lift-constraint to lists. We obtain a list of terms.

Definitions and Theorems

Function: lift-constraint-list

(defun lift-constraint-list (constrs prime state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (constraint-listp constrs)
                              (symbolp prime))))
  (let ((__function__ 'lift-constraint-list))
    (declare (ignorable __function__))
    (cond ((endp constrs) nil)
          (t (cons (lift-constraint (car constrs)
                                    prime state)
                   (lift-constraint-list (cdr constrs)
                                         prime state))))))

Theorem: true-listp-of-lift-constraint-list

(defthm true-listp-of-lift-constraint-list
  (b* ((terms (lift-constraint-list constrs prime state)))
    (true-listp terms))
  :rule-classes :rewrite)