		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))