Shallowly embedded semanics of a list of definitions.
(sesem-definition-list defs prime state) → events
This is the list of events generated from the definitions.
Function:
(defun sesem-definition-list (defs prime state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (definition-listp defs) (symbolp prime)))) (let ((__function__ 'sesem-definition-list)) (declare (ignorable __function__)) (cond ((endp defs) nil) (t (cons (sesem-definition (car defs) prime state) (sesem-definition-list (cdr defs) prime state))))))
Theorem:
(defthm pseudo-event-form-listp-of-sesem-definition-list (b* ((events (sesem-definition-list defs prime state))) (pseudo-event-form-listp events)) :rule-classes :rewrite)