		Search-engine friendly clone of the ACL2 documentation.

Grammar

grammar-rules

The JSON grammar rules from RFC 8259.

The file grammar.abnf contains the grammar rules, copied and pasted from RFC 8259. The ABNF grammar parser and abstractor are used to build an ACL2 representation of the JSON grammar rules, excluding the referenced ABNF core rules.

The JSON grammar rules are well-formed.

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

Definitions and Theorems

Function: untranslate-preprocess-*grammar-rules*

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

Theorem: rulelist-wfp-of-*grammar-rules*

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