		Search-engine friendly clone of the ACL2 documentation.

Values

Int-value-numbits

Returns the number of bits that a value of this kind could take.

Signature
(int-value-numbits int-v) → result
Arguments: int-v — Guard (int-valuep int-v).
Returns: result — Type (natp result), given the guard.

The integer value of int-v is ignored; just its kind is looked at. The size of the kind in bits is returned.

Definitions and Theorems

Function: int-value-numbits

(defun int-value-numbits (int-v)
  (declare (xargs :guard (int-valuep int-v)))
  (let ((__function__ 'int-value-numbits))
    (declare (ignorable __function__))
    (case (value-kind int-v)
      (:u8 8)
      (:u16 16)
      (:u32 32)
      (:u64 64)
      (:u128 128)
      (:i8 8)
      (:i16 16)
      (:i32 32)
      (:i64 64)
      (:i128 128)
      (t (prog2$ (impossible) 0)))))

Theorem: natp-of-int-value-numbits

(defthm natp-of-int-value-numbits
  (implies (and (int-valuep int-v))
           (b* ((result (int-value-numbits int-v)))
             (natp result)))
  :rule-classes :rewrite)