Generate a parsing function for a specification.
(defdefparse-gen-function-for-spec spec rules prefix group-table option-table repetition-table) → event
Function:
(defun defdefparse-gen-function-for-spec (spec rules prefix group-table option-table repetition-table) (declare (xargs :guard (and (defdefparse-function-spec-p spec) (rulelistp rules) (common-lisp::symbolp prefix) (defdefparse-alt-symbol-alistp group-table) (defdefparse-alt-symbol-alistp option-table) (defdefparse-rep-symbol-alistp repetition-table)))) (let ((__function__ 'defdefparse-gen-function-for-spec)) (declare (ignorable __function__)) (defdefparse-function-spec-case spec :rulename (defdefparse-gen-function-for-rulename spec.get spec.order rules prefix group-table option-table repetition-table) :group (defdefparse-gen-function-for-group spec.get spec.order prefix group-table option-table repetition-table) :option (defdefparse-gen-function-for-option spec.get spec.order prefix group-table option-table repetition-table) :repetition (defdefparse-gen-function-for-repetition spec.get prefix group-table option-table repetition-table))))
Theorem:
(defthm maybe-pseudo-event-formp-of-defdefparse-gen-function-for-spec (b* ((event (defdefparse-gen-function-for-spec spec rules prefix group-table option-table repetition-table))) (acl2::maybe-pseudo-event-formp event)) :rule-classes :rewrite)