		Search-engine friendly clone of the ACL2 documentation.

Grammar

grammar

The parsed ABNF grammar of Leo.

We parse the grammar file to obtain an ABNF grammar value.

We prove that the grammar is well-formed, is closed, and only generates terminals in the Unicode character set.

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* (integers-from-to 0 1114111)))

Subtopics

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