		Search-engine friendly clone of the ACL2 documentation.

Meta-circular-validation

concrete-syntax-rules-parsed

Parse tree of the text that contains the concrete syntax rules of ABNF.

The file concrete-syntax-rules.abnf contains the definition of the concrete syntax 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 definition of the concrete syntax of ABNF without errors.

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

Definitions and Theorems

Function: untranslate-preprocess-*concrete-syntax-rules-parsed*

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

Theorem: treep-of-*concrete-syntax-rules-parsed*

(defthm treep-of-*concrete-syntax-rules-parsed*
  (treep *concrete-syntax-rules-parsed*))