		Search-engine friendly clone of the ACL2 documentation.

Grammar

grammar

The parsed ABNF grammar of the AleoVM language.

We parse and abstract 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*.