		Search-engine friendly clone of the ACL2 documentation.

Character-value-retrieval

Rule-char-vals

Set of character value notations in a rule.

Signature
(rule-char-vals rule) → charvals
Arguments: rule — Guard (rulep rule).
Returns: charvals — Type (char-val-setp charvals).

This is the set of character value notations in the alternation that defines the rules.

Definitions and Theorems

Function: rule-char-vals

(defun rule-char-vals (rule)
  (declare (xargs :guard (rulep rule)))
  (let ((__function__ 'rule-char-vals))
    (declare (ignorable __function__))
    (alternation-char-vals (rule->definiens rule))))

Theorem: char-val-setp-of-rule-char-vals

(defthm char-val-setp-of-rule-char-vals
  (b* ((charvals (rule-char-vals rule)))
    (char-val-setp charvals))
  :rule-classes :rewrite)

Theorem: rule-char-vals-of-rule-fix-rule

(defthm rule-char-vals-of-rule-fix-rule
  (equal (rule-char-vals (rule-fix rule))
         (rule-char-vals rule)))

Theorem: rule-char-vals-rule-equiv-congruence-on-rule

(defthm rule-char-vals-rule-equiv-congruence-on-rule
  (implies (rule-equiv rule rule-equiv)
           (equal (rule-char-vals rule)
                  (rule-char-vals rule-equiv)))
  :rule-classes :congruence)