		Search-engine friendly clone of the ACL2 documentation.

Types

Integer-type-bits-nulfun

Name of the nullary function that defines the size in bits of a C integer type.

Signature
(integer-type-bits-nulfun type) → bits
Arguments: type — Guard (typep type).
Returns: bits — Type (symbolp bits).

This is the name of one of the nullary functions introduced in integer-formats.

We take the name of the kind, remove the initial s or u, and add -bits at the end.

Definitions and Theorems

Function: integer-type-bits-nulfun

(defun integer-type-bits-nulfun (type)
 (declare (xargs :guard (typep type)))
 (declare (xargs :guard (type-integerp type)))
 (let ((__function__ 'integer-type-bits-nulfun))
  (declare (ignorable __function__))
  (b*
   ((char/short/int/long/llong
     (if (type-case type :char)
         "CHAR"
       (implode
            (cdr (acl2::explode (symbol-name (type-kind type))))))))
   (pack char/short/int/long/llong '-bits))))

Theorem: symbolp-of-integer-type-bits-nulfun

(defthm symbolp-of-integer-type-bits-nulfun
  (b* ((bits (integer-type-bits-nulfun type)))
    (symbolp bits))
  :rule-classes :rewrite)

Theorem: integer-type-bits-nulfun-of-type-fix-type

(defthm integer-type-bits-nulfun-of-type-fix-type
  (equal (integer-type-bits-nulfun (type-fix type))
         (integer-type-bits-nulfun type)))

Theorem: integer-type-bits-nulfun-type-equiv-congruence-on-type

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