		Search-engine friendly clone of the ACL2 documentation.
Integer-formats
Def-integer-bits

Macro to generate the nullary functions, and some theorems about them, for the size in bits of the C integer types.
Macro: def-integer-bits
(defmacro def-integer-bits (type bits minbits)
 (declare
    (xargs :guard (and (member-eq type '(char short int long llong))
                       (posp bits)
                       (posp minbits)
                       (>= bits minbits))))
 (b* ((type-bits (pack type '-bits))
      (type-bits-bound (pack type-bits '-bound))
      (type-bits-multiple-of-char-bits
           (pack type '-bits-multiple-of-char-bits))
      (short-substring (if (eq type 'char)
                           "signed, unsigned, and plain"
                         "signed and unsigned")))
  (cons
   'define
   (cons
    type-bits
    (cons
     'nil
     (cons
      ':returns
      (cons
       (cons type-bits
             '(posp :rule-classes :type-prescription))
       (cons
        ':short
        (cons
         (str::cat "Size of " short-substring " @('"
                   (str::downcase-string (symbol-name type))
                   "') values, in bits.")
         (cons
          bits
          (cons
           '///
           (append
            (and
             (not (eq type 'char))
             (cons
              (cons
               'defrule
               (cons
                 type-bits-multiple-of-char-bits
                 (cons (cons 'integerp
                             (cons (cons '/
                                         (cons (cons type-bits 'nil)
                                               '((char-bits))))
                                   'nil))
                       '(:rule-classes :type-prescription
                                       :enable char-bits))))
              'nil))
            (cons
             (cons
                  'in-theory
                  (cons (cons 'disable
                              (cons (cons ':e (cons type-bits 'nil))
                                    'nil))
                        'nil))
             (cons
              (cons
               'defret
               (cons
                   type-bits-bound
                   (cons (cons '>=
                               (cons type-bits (cons minbits 'nil)))
                         '(:rule-classes :linear))))
              'nil))))))))))))))