Rule list that *core-rules-parsed* abstracts to.
Applying the grammar abstractor to the parse tree
obtained by applying the grammar parser to the file
Furthermore, the rule list thus obtained is identical *core-rules*, which is the definition of the concrete syntax of ABNF written manually using the abstract syntax of ABNF.
We use add-const-to-untranslate-preprocess to keep this constant unexpanded in output.
Definition:
(defconst *core-rules-parsed-and-abstracted* (abstract-rulelist *core-rules-parsed*))
Function:
(defun untranslate-preprocess-*core-rules-parsed-and-abstracted* (acl2::term acl2::wrld) (if (equal acl2::term (list 'quote *core-rules-parsed-and-abstracted*)) '*core-rules-parsed-and-abstracted* (untranslate-preprocess-*concrete-syntax-rules-parsed* acl2::term acl2::wrld)))
Theorem:
(defthm *core-rules-parsed-and-abstracted*-correct (equal *core-rules-parsed-and-abstracted* *core-rules*) :rule-classes nil)