Generate the specialized matching predicates.
(deftreeops-gen-matchers grammar prefix) → events
Function:
(defun deftreeops-gen-matchers (grammar prefix) (declare (xargs :guard (and (common-lisp::symbolp grammar) (common-lisp::symbolp prefix)))) (let ((__function__ 'deftreeops-gen-matchers)) (declare (ignorable __function__)) (append (deftreeops-gen-cst-match grammar prefix) (deftreeops-gen-cst-list-elem-match grammar prefix) (deftreeops-gen-cst-list-rep-match grammar prefix) (deftreeops-gen-cst-list-list-conc-match grammar prefix) (deftreeops-gen-cst-list-list-alt-match grammar prefix))))
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-matchers (b* ((events (deftreeops-gen-matchers grammar prefix))) (pseudo-event-form-listp events)) :rule-classes :rewrite)