		Search-engine friendly clone of the ACL2 documentation.

Semantics-shallowly-embedded

Sesem-constraint-list

Shallowly embedded semantics of a list of constraints.

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

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

Definitions and Theorems

Function: sesem-constraint-list

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

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

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