Recognizer of Leo integer values.
(int-valuep x) → yes/no
These are the unsigned and signed integer values.
We use this function as an abbreviation, so we leave it enabled. Rules triggered by this function should be generally avoided.
Function:
(defun int-valuep (x) (declare (xargs :guard t)) (let ((__function__ 'int-valuep)) (declare (ignorable __function__)) (and (valuep x) (member-eq (value-kind x) '(:u8 :u16 :u32 :u64 :u128 :i8 :i16 :i32 :i64 :i128)) t)))
Theorem:
(defthm booleanp-of-int-valuep (b* ((yes/no (int-valuep x))) (booleanp yes/no)) :rule-classes :rewrite)