		Search-engine friendly clone of the ACL2 documentation.

Semantics-shallowly-embedded

Sesem-expression-list

Shallowly embedded semantics of lists of expressions.

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

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

Definitions and Theorems

Function: sesem-expression-list

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

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

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