Generate the events for all the character value notations in the alist.
(deftreeops-gen-charval-alist-events charval-infos prefix) → (mv leafterm-thm-events event-alist)
Function:
(defun deftreeops-gen-charval-alist-events (charval-infos prefix) (declare (xargs :guard (and (deftreeops-charval-info-alistp charval-infos) (common-lisp::symbolp prefix)))) (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)) ((mv more-leafterm-thm-events more-event-alist) (deftreeops-gen-charval-alist-events (cdr charval-infos) prefix))) (mv (cons leafterm-thm-events more-leafterm-thm-events) (append event-alist more-event-alist)))))
Theorem:
(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))) (pseudo-event-form-listp leafterm-thm-events)) :rule-classes :rewrite)
Theorem:
(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))) (symbol-pseudoeventform-alistp event-alist)) :rule-classes :rewrite)