		Search-engine friendly clone of the ACL2 documentation.

Integer-format-templates

Integer-format->bit-size

Number of bits of an integer format.

Signature
(integer-format->bit-size format) → size
Arguments: format — Guard (integer-formatp format).
Returns: size — Type (posp size).

This is the total number of bits of the unsigned or signed format: the two have the same number of bits, because of uinteger-sinteger-bit-roles-wfp.

Definitions and Theorems

Function: integer-format->bit-size

(defun integer-format->bit-size (format)
  (declare (xargs :guard (integer-formatp format)))
  (len (uinteger-format->bits (uinteger+sinteger-format->unsigned
                                   (integer-format->pair format)))))

Theorem: posp-of-integer-format->bit-size

(defthm posp-of-integer-format->bit-size
  (b* ((size (integer-format->bit-size format)))
    (posp size))
  :rule-classes :rewrite)

Theorem: integer-format->bit-size-alt-def

(defthm integer-format->bit-size-alt-def
 (equal
  (integer-format->bit-size format)
  (len
      (sinteger-format->bits (uinteger+sinteger-format->signed
                                  (integer-format->pair format))))))

Theorem: integer-format->bit-size-type-prescription

(defthm integer-format->bit-size-type-prescription
  (implies (integer-formatp format)
           (b* ((?size (integer-format->bit-size format)))
             (and (posp size) (> size 1))))
  :rule-classes :type-prescription)

Theorem: integer-format->bit-size-of-integer-format-fix-format

(defthm integer-format->bit-size-of-integer-format-fix-format
  (equal (integer-format->bit-size (integer-format-fix format))
         (integer-format->bit-size format)))

Theorem: integer-format->bit-size-integer-format-equiv-congruence-on-format

(defthm
 integer-format->bit-size-integer-format-equiv-congruence-on-format
 (implies (integer-format-equiv format format-equiv)
          (equal (integer-format->bit-size format)
                 (integer-format->bit-size format-equiv)))
 :rule-classes :congruence)