		Search-engine friendly clone of the ACL2 documentation.

Dec-digit

Dec-digitp

Recognizer for dec-digit.

Signature
(dec-digitp x) → yes/no
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: dec-digitp

(defun dec-digitp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'dec-digitp))
    (declare (ignorable __function__))
    (and (integerp x)
         (<= (char-code #\0) x)
         (<= x (char-code #\9)))))

Theorem: booleanp-of-dec-digitp

(defthm booleanp-of-dec-digitp
  (b* ((yes/no (dec-digitp x)))
    (booleanp yes/no))
  :rule-classes :rewrite)