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:
(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*))
Function:
(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:
(defthm rulelistp-of-*concrete-syntax-rules* (rulelistp *concrete-syntax-rules*))