		Search-engine friendly clone of the ACL2 documentation.

Expdata-event-generation

Expdata-gen-defsurjs

Generate all the local defsurjs from a list.

Signature
(expdata-gen-defsurjs surjmaps verify-guards$ print$) → events
Arguments: surjmaps — Guard (expdata-surjmap-listp surjmaps).; verify-guards$ — Guard (booleanp verify-guards$).; print$ — Guard (evmac-input-print-p print$).
Returns: events — Type (pseudo-event-form-listp events).

Definitions and Theorems

Function: expdata-gen-defsurjs

(defun expdata-gen-defsurjs (surjmaps verify-guards$ print$)
  (declare (xargs :guard (and (expdata-surjmap-listp surjmaps)
                              (booleanp verify-guards$)
                              (evmac-input-print-p print$))))
  (let ((__function__ 'expdata-gen-defsurjs))
    (declare (ignorable __function__))
    (b* (((when (endp surjmaps)) nil)
         (surjmap (car surjmaps)))
      (if (expdata-surjmap->localp surjmap)
          (cons (expdata-gen-defsurj surjmap verify-guards$ print$)
                (expdata-gen-defsurjs (cdr surjmaps)
                                      verify-guards$ print$))
        (expdata-gen-defsurjs (cdr surjmaps)
                              verify-guards$ print$)))))

Theorem: pseudo-event-form-listp-of-expdata-gen-defsurjs

(defthm pseudo-event-form-listp-of-expdata-gen-defsurjs
  (b*
    ((events (expdata-gen-defsurjs surjmaps verify-guards$ print$)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)