		Search-engine friendly clone of the ACL2 documentation.

Dec-digit-fix

Fixer for dec-digit.

Function: dec-digit-fix

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

Theorem: dec-digitp-of-dec-digit-fix

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

Theorem: dec-digit-fix-when-dec-digitp

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