The ACL2 integer value of
We prefer to use dash instead of underscore, since it's more common convention in ACL2. We also prefer the plural `bits', since it's a number of bits.
Function:
(defun ienv->char-bits (ienv) (declare (xargs :guard (ienvp ienv))) (let ((__function__ 'ienv->char-bits)) (declare (ignorable __function__)) (uchar-format->bits (ienv->uchar-format ienv))))
Theorem:
(defthm posp-of-ienv->char-bits (b* ((bits (ienv->char-bits ienv))) (posp bits)) :rule-classes :rewrite)
Theorem:
(defthm ienv->char-bits-type-prescription (b* ((?bits (ienv->char-bits ienv))) (and (posp bits) (> bits 1))) :rule-classes :type-prescription)
Theorem:
(defthm ienv->char-bits-lower-bound (b* ((?bits (ienv->char-bits ienv))) (>= bits 8)) :rule-classes :linear)
Theorem:
(defthm ienv->char-bits-of-ienv-fix-ienv (equal (ienv->char-bits (ienv-fix ienv)) (ienv->char-bits ienv)))
Theorem:
(defthm ienv->char-bits-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (ienv->char-bits ienv) (ienv->char-bits ienv-equiv))) :rule-classes :congruence)