		Search-engine friendly clone of the ACL2 documentation.

Int-bits

Size of signed and unsigned int values, in bits.

Function: int-bits

(defun int-bits nil
  (declare (xargs :guard t))
  (let ((__function__ 'int-bits))
    (declare (ignorable __function__))
    32))

Theorem: posp-of-int-bits

(defthm posp-of-int-bits
  (b* ((int-bits (int-bits)))
    (posp int-bits))
  :rule-classes :type-prescription)

Theorem: int-bits-multiple-of-char-bits

(defthm int-bits-multiple-of-char-bits
  (integerp (/ (int-bits) (char-bits)))
  :rule-classes :type-prescription)

Theorem: int-bits-bound

(defthm int-bits-bound
  (b* ((?int-bits (int-bits)))
    (>= int-bits 16))
  :rule-classes :linear)