|
|
|---|
|
|
|
|---|
Constraints on the value of
(char-bit-constrp char-bit) → yes/no
It must be an integer that is at least 8.
Function:
(defun char-bit-constrp (char-bit) (declare (xargs :guard t)) (and (integerp char-bit) (>= char-bit 8)))
Theorem:
(defthm booleanp-of-char-bit-constrp (b* ((yes/no (char-bit-constrp char-bit))) (booleanp yes/no)) :rule-classes :rewrite)