		Search-engine friendly clone of the ACL2 documentation.

Chareqv

Case-sensitive character equivalence test.

(chareqv x y) determines if x and y are equivalent when interpreted as characters. That is, non-characters are first coerced to be the NUL character (via char-fix), then we see if these coerced arguments are equal.

See also str::ichareqv for a case-insensitive alternative.

Definitions and Theorems

Function: chareqv$inline

(defun chareqv$inline (x y)
       (declare (xargs :guard t))
       (eql (char-fix x) (char-fix y)))

Theorem: chareqv-is-an-equivalence

(defthm chareqv-is-an-equivalence
        (and (booleanp (chareqv x y))
             (chareqv x x)
             (implies (chareqv x y) (chareqv y x))
             (implies (and (chareqv x y) (chareqv y z))
                      (chareqv x z)))
        :rule-classes (:equivalence))

Theorem: chareqv-of-char-fix

(defthm chareqv-of-char-fix
        (chareqv (char-fix x) x))

Theorem: chareqv-implies-equal-char-fix-1

(defthm chareqv-implies-equal-char-fix-1
        (implies (chareqv x x-equiv)
                 (equal (char-fix x) (char-fix x-equiv)))
        :rule-classes (:congruence))

Theorem: chareqv-implies-equal-char-code-1

(defthm chareqv-implies-equal-char-code-1
        (implies (chareqv x x-equiv)
                 (equal (char-code x)
                        (char-code x-equiv)))
        :rule-classes (:congruence))

Theorem: chareqv-implies-equal-char<-1

(defthm chareqv-implies-equal-char<-1
        (implies (chareqv x x-equiv)
                 (equal (char< x y) (char< x-equiv y)))
        :rule-classes (:congruence))

Theorem: chareqv-implies-equal-char<-2

(defthm chareqv-implies-equal-char<-2
        (implies (chareqv y y-equiv)
                 (equal (char< x y) (char< x y-equiv)))
        :rule-classes (:congruence))