		Search-engine friendly clone of the ACL2 documentation.

Types

Integer-type-minbits

Minimum number of bits that forms a value of a C integer type.

Signature
(integer-type-minbits type) → minbits
Arguments: type — Guard (typep type).
Returns: minbits — Type (posp minbits).

Definitions and Theorems

Function: integer-type-minbits

(defun integer-type-minbits (type)
  (declare (xargs :guard (typep type)))
  (declare (xargs :guard (type-integerp type)))
  (let ((__function__ 'integer-type-minbits))
    (declare (ignorable __function__))
    (case (type-kind type)
      ((:char :schar :uchar) 8)
      ((:sshort :ushort) 16)
      ((:sint :uint) 16)
      ((:slong :ulong) 32)
      ((:sllong :ullong) 64)
      (t (prog2$ (impossible) 1)))))

Theorem: posp-of-integer-type-minbits

(defthm posp-of-integer-type-minbits
  (b* ((minbits (integer-type-minbits type)))
    (posp minbits))
  :rule-classes :type-prescription)

Theorem: integer-type-minbits-of-type-fix-type

(defthm integer-type-minbits-of-type-fix-type
  (equal (integer-type-minbits (type-fix type))
         (integer-type-minbits type)))

Theorem: integer-type-minbits-type-equiv-congruence-on-type

(defthm integer-type-minbits-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (integer-type-minbits type)
                  (integer-type-minbits type-equiv)))
  :rule-classes :congruence)