		Search-engine friendly clone of the ACL2 documentation.

Hex-digit-fix

Fixer for hex-digit.

Function: hex-digit-fix

(defun hex-digit-fix (x)
  (declare (xargs :guard (hex-digitp x)))
  (mbe :logic (if (hex-digitp x) x (char-code #\0))
       :exec x))

Theorem: hex-digitp-of-hex-digit-fix

(defthm hex-digitp-of-hex-digit-fix
  (b* ((fixed-x (hex-digit-fix x)))
    (hex-digitp fixed-x))
  :rule-classes :rewrite)

Theorem: hex-digit-fix-when-hex-digitp

(defthm hex-digit-fix-when-hex-digitp
  (implies (hex-digitp x)
           (equal (hex-digit-fix x) x)))