Recognizer for non-zero numeric characters (1-9).
(nonzero-dec-digit-char-p x) → bool
Function:
(defun nonzero-dec-digit-char-p$inline (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'nonzero-dec-digit-char-p)) (declare (ignorable acl2::__function__)) (mbe :logic (let ((code (char-code (char-fix x)))) (and (<= (char-code #\1) code) (<= code (char-code #\9)))) :exec (and (characterp x) (let ((code (the (unsigned-byte 8) (char-code (the character x))))) (declare (type (unsigned-byte 8) code)) (and (<= (the (unsigned-byte 8) code) (the (unsigned-byte 8) 57)) (<= (the (unsigned-byte 8) 49) (the (unsigned-byte 8) code))))))))
Theorem:
(defthm ichareqv-implies-equal-nonzero-dec-digit-char-p-1 (implies (ichareqv x x-equiv) (equal (nonzero-dec-digit-char-p x) (nonzero-dec-digit-char-p x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm dec-digit-char-p-when-nonzero-dec-digit-char-p (implies (nonzero-dec-digit-char-p x) (dec-digit-char-p x)))