		Search-engine friendly clone of the ACL2 documentation.

Core-rules

core-rules

All the core rules.

Properties of the core rules are proved in core-rules-validation.

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

Definition: *core-rules*

(defconst *core-rules*
  (list *rule_alpha*
        *rule_bit* *rule_char* *rule_cr*
        *rule_crlf* *rule_ctl* *rule_digit*
        *rule_dquote* *rule_hexdig* *rule_htab*
        *rule_lf* *rule_lwsp* *rule_octet*
        *rule_sp* *rule_vchar* *rule_wsp*))

Definitions and Theorems

Function: untranslate-preprocess-*core-rules*

(defun untranslate-preprocess-*core-rules* (acl2::term acl2::wrld)
  (if (equal acl2::term (list 'quote *core-rules*))
      '*core-rules*
    (acl2::untranslate-preproc-for-define acl2::term acl2::wrld)))

Theorem: rulelistp-of-*core-rules*

(defthm rulelistp-of-*core-rules*
  (rulelistp *core-rules*))