code-char-char-code-with-force

other

(in-package "ACL2")

code-char-char-code-is-identity-forcedtheorem

(defthm code-char-char-code-is-identity-forced
  (implies (force (characterp c))
    (equal (code-char (char-code c)) c)))

char-code-code-char-is-identity-forcedtheorem

(defthm char-code-code-char-is-identity-forced
  (implies (and (force (integerp n))
      (force (<= 0 n))
      (force (< n 256)))
    (equal (char-code (code-char n)) n)))