Generate the events for all the character value notations in the alist.
(deftreeops-gen-charval-alist-events charval-infos prefix) → leafterm-thm-events
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)) nil) ((cons charval info) (car charval-infos)) (leafterm-thm-events (deftreeops-gen-charval-events charval info prefix)) (leafterm-thm-more-events (deftreeops-gen-charval-alist-events (cdr charval-infos) prefix))) (cons leafterm-thm-events leafterm-thm-more-events))))
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-charval-alist-events (b* ((leafterm-thm-events (deftreeops-gen-charval-alist-events charval-infos prefix))) (pseudo-event-form-listp leafterm-thm-events)) :rule-classes :rewrite)