(vl-consteval-basictype-bits type) → (mv ok res)
Function:
(defun vl-consteval-basictype-bits (type) (declare (xargs :guard (vl-basictype-p type))) (let ((__function__ 'vl-consteval-basictype-bits)) (declare (ignorable __function__)) (b* (((vl-basictype type))) (case type.kind (:vl-byte (mv t 8)) (:vl-shortint (mv t 16)) (:vl-longint (mv t 64)) (:vl-integer (mv t 32)) (:vl-time (mv t 64)) (:vl-bit (mv t 1)) (:vl-logic (mv t 1)) (:vl-reg (mv t 1)) (otherwise (mv nil nil))))))
Theorem:
(defthm booleanp-of-vl-consteval-basictype-bits.ok (b* (((mv ?ok ?res) (vl-consteval-basictype-bits type))) (booleanp ok)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-consteval-basictype-bits.res (b* (((mv ?ok ?res) (vl-consteval-basictype-bits type))) (implies ok (posp res))) :rule-classes :type-prescription)
Theorem:
(defthm vl-consteval-basictype-bits-of-vl-basictype-fix-type (equal (vl-consteval-basictype-bits (vl-basictype-fix type)) (vl-consteval-basictype-bits type)))
Theorem:
(defthm vl-consteval-basictype-bits-vl-basictype-equiv-congruence-on-type (implies (vl-basictype-equiv type type-equiv) (equal (vl-consteval-basictype-bits type) (vl-consteval-basictype-bits type-equiv))) :rule-classes :congruence)