		Search-engine friendly clone of the ACL2 documentation.

Meta-circular-validation

core-rules-parsed

Parse tree of the text that contains the core rules.

The file core-rules.abnf contains the definition of the core rules of ABNF using the concrete syntax of ABNF itself, copied and pasted from [RFC]. Calling parse-grammar-from-file on that file yields a parse tree. This shows that the executable grammar parser parses the core rules of ABNF without errors.

We use add-const-to-untranslate-preprocess to keep this constant unexpanded in output.

Definitions and Theorems

Function: untranslate-preprocess-*core-rules-parsed*

(defun untranslate-preprocess-*core-rules-parsed*
       (acl2::term acl2::wrld)
  (if (equal acl2::term
             (list 'quote *core-rules-parsed*))
      '*core-rules-parsed*
    (untranslate-preprocess-*grammar* acl2::term acl2::wrld)))

Theorem: treep-of-*core-rules-parsed*

(defthm treep-of-*core-rules-parsed*
  (treep *core-rules-parsed*))