		Search-engine friendly clone of the ACL2 documentation.

Concrete-syntax

grammar

Grammar of ABNF.

The ABNF grammar of ABNF consists of the concrete syntax rules and the core rules that they reference (directly and indirectly).

Properties of these rules are proved in concrete-syntax-validation.

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

Definition: *grammar*

(defconst *grammar*
  (append *concrete-syntax-rules*
          (list *rule_alpha* *rule_bit* *rule_cr*
                *rule_crlf* *rule_digit* *rule_dquote*
                *rule_hexdig* *rule_htab* *rule_lf*
                *rule_sp* *rule_vchar* *rule_wsp*)))

Definitions and Theorems

Function: untranslate-preprocess-*grammar*

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

Theorem: rulelistp-of-*grammar*

(defthm rulelistp-of-*grammar*
  (rulelistp *grammar*))