		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-event-generation

Deftreeops-gen-charval-alist-events

Generate the events for all the character value notations in the alist.

Signature
(deftreeops-gen-charval-alist-events charval-infos prefix print) → (mv leafterm-thm-events event-alist)
Arguments: charval-infos — Guard (deftreeops-charval-info-alistp charval-infos).; prefix — Guard (common-lisp::symbolp prefix).; print — Guard (evmac-input-print-p print).
Returns: leafterm-thm-events — Type (pseudo-event-form-listp leafterm-thm-events).; event-alist — Type (symbol-pseudoeventform-alistp event-alist).

Definitions and Theorems

Function: deftreeops-gen-charval-alist-events

(defun deftreeops-gen-charval-alist-events
       (charval-infos prefix print)
 (declare
   (xargs :guard (and (deftreeops-charval-info-alistp charval-infos)
                      (common-lisp::symbolp prefix)
                      (evmac-input-print-p print))))
 (let ((__function__ 'deftreeops-gen-charval-alist-events))
   (declare (ignorable __function__))
   (b* (((when (endp charval-infos))
         (mv nil nil))
        ((cons charval info)
         (car charval-infos))
        ((mv leafterm-thm-events event-alist)
         (deftreeops-gen-charval-events charval info prefix print))
        ((mv more-leafterm-thm-events
             more-event-alist)
         (deftreeops-gen-charval-alist-events (cdr charval-infos)
                                              prefix print)))
     (mv (append leafterm-thm-events
                 more-leafterm-thm-events)
         (append event-alist more-event-alist)))))

Theorem: pseudo-event-form-listp-of-deftreeops-gen-charval-alist-events.leafterm-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-charval-alist-events.leafterm-thm-events
 (b* (((mv ?leafterm-thm-events ?event-alist)
       (deftreeops-gen-charval-alist-events
            charval-infos prefix print)))
   (pseudo-event-form-listp leafterm-thm-events))
 :rule-classes :rewrite)

Theorem: symbol-pseudoeventform-alistp-of-deftreeops-gen-charval-alist-events.event-alist

(defthm
 symbol-pseudoeventform-alistp-of-deftreeops-gen-charval-alist-events.event-alist
 (b* (((mv ?leafterm-thm-events ?event-alist)
       (deftreeops-gen-charval-alist-events
            charval-infos prefix print)))
   (symbol-pseudoeventform-alistp event-alist))
 :rule-classes :rewrite)