Fixer for hex-digit-char.
(hex-digit-char-fix x) → fixed-x
Function:
(defun hex-digit-char-fix (x) (declare (xargs :guard (hex-digit-char-p x))) (mbe :logic (if (hex-digit-char-p x) x #\0) :exec x))
Theorem:
(defthm hex-digit-char-p-of-hex-digit-char-fix (b* ((fixed-x (hex-digit-char-fix x))) (hex-digit-char-p fixed-x)) :rule-classes :rewrite)
Theorem:
(defthm hex-digit-char-fix-when-hex-digit-char-p (implies (hex-digit-char-p x) (equal (hex-digit-char-fix x) x)))