		Search-engine friendly clone of the ACL2 documentation.

Oct-digit

Oct-digitp

Recognizer for oct-digit.

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

Definitions and Theorems

Function: oct-digitp

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

Theorem: booleanp-of-oct-digitp

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