		Search-engine friendly clone of the ACL2 documentation.

Grammar

grammar

The ABNF grammar represented in ACL2.

We use our verified grammar parser and our abstractor to turn the grammar in the grammar.abnf file into an ACL2 representation.

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

We show that the grammar is well-formed, closed, and Unicode.

Definitions and Theorems

Function: untranslate-preprocess-*grammar*

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

Theorem: rulelist-wfp-of-*grammar*

(defthm rulelist-wfp-of-*grammar*
  (abnf::rulelist-wfp *grammar*))

Theorem: rulelist-closedp-of-*grammar*

(defthm rulelist-closedp-of-*grammar*
  (abnf::rulelist-closedp *grammar*))

Theorem: unicode-only-*grammar*

(defthm unicode-only-*grammar*
  (abnf::rulelist-in-termset-p *grammar*
                               (acl2::integers-from-to 0 1114111)))

Subtopics

*grammar*-tree-operations: Tree operations specialized to *grammar*.