		Search-engine friendly clone of the ACL2 documentation.

Concrete-syntax-rules

concrete-syntax-rules

The ABNF concrete syntax rules, excluding the core rules.

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

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

Definition: *concrete-syntax-rules*

(defconst *concrete-syntax-rules*
  (list *rule_rulelist*
        *rule_rule* *rule_rulename*
        *rule_defined-as* *rule_elements*
        *rule_c-wsp* *rule_c-nl* *rule_comment*
        *rule_alternation* *rule_concatenation*
        *rule_repetition* *rule_repeat*
        *rule_element* *rule_group*
        *rule_option* *rule_char-val*
        *rule_case-insensitive-string*
        *rule_case-sensitive-string*
        *rule_quoted-string* *rule_num-val*
        *rule_bin-val* *rule_dec-val*
        *rule_hex-val* *rule_prose-val*))

Definitions and Theorems

Function: untranslate-preprocess-*concrete-syntax-rules*

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

Theorem: rulelistp-of-*concrete-syntax-rules*

(defthm rulelistp-of-*concrete-syntax-rules*
  (rulelistp *concrete-syntax-rules*))