		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-defisos

Generate all the local defisos from a list.

Signature
(isodata-gen-defisos isomaps verify-guards$ print$) → events
Arguments: isomaps — Guard (isodata-isomap-listp isomaps).; 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: isodata-gen-defisos

(defun isodata-gen-defisos (isomaps verify-guards$ print$)
  (declare (xargs :guard (and (isodata-isomap-listp isomaps)
                              (booleanp verify-guards$)
                              (evmac-input-print-p print$))))
  (let ((__function__ 'isodata-gen-defisos))
    (declare (ignorable __function__))
    (b* (((when (endp isomaps)) nil)
         (isomap (car isomaps)))
      (if (isodata-isomap->localp isomap)
          (cons (isodata-gen-defiso isomap verify-guards$ print$)
                (isodata-gen-defisos (cdr isomaps)
                                     verify-guards$ print$))
        (isodata-gen-defisos (cdr isomaps)
                             verify-guards$ print$)))))

Theorem: pseudo-event-form-listp-of-isodata-gen-defisos

(defthm pseudo-event-form-listp-of-isodata-gen-defisos
  (b* ((events (isodata-gen-defisos isomaps verify-guards$ print$)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)