Generate the table of repetition parsing functions.
(defdefparse-gen-repetition-table args prefix table-name) → event
We generate a named constant defined with the alist produced by defdefparse-gen-repetition-alist.
Function:
(defun defdefparse-gen-repetition-table (args prefix table-name) (declare (xargs :guard (and (true-listp args) (common-lisp::symbolp prefix) (common-lisp::symbolp table-name)))) (let ((__function__ 'defdefparse-gen-repetition-table)) (declare (ignorable __function__)) (b* ((alist (defdefparse-gen-repetition-alist args prefix))) (cons 'defval (cons table-name (cons ':short (cons '"Table of repetition parsing functions." (cons (cons 'quote (cons alist 'nil)) (cons '/// (cons (cons 'assert-event (cons (cons 'defdefparse-rep-symbol-alistp (cons table-name 'nil)) 'nil)) (cons (cons 'assert-event (cons (cons 'no-duplicatesp-equal (cons (cons 'strip-cars (cons table-name 'nil)) 'nil)) 'nil)) (cons (cons 'assert-event (cons (cons 'no-duplicatesp-eq (cons (cons 'strip-cdrs (cons table-name 'nil)) 'nil)) 'nil)) 'nil))))))))))))
Theorem:
(defthm pseudo-event-formp-of-defdefparse-gen-repetition-table (b* ((event (defdefparse-gen-repetition-table args prefix table-name))) (pseudo-event-formp event)) :rule-classes :rewrite)