		Search-engine friendly clone of the ACL2 documentation.

Integer-ranges

Integer-type-max

Maximum mathematical integer value of an integer type.

Signature
(integer-type-max type) → min
Arguments: type — Guard (typep type).
Returns: min — Type (integerp min).

For now we exclude the plain char type, via the guard. However, we prefer to keep the name of this function more general, in anticipation for extending it to those two types.

Definitions and Theorems

Function: integer-type-max

(defun integer-type-max (type)
  (declare (xargs :guard (typep type)))
  (declare (xargs :guard (type-nonchar-integerp type)))
  (cond ((type-case type :schar) (schar-max))
        ((type-case type :uchar) (uchar-max))
        ((type-case type :sshort) (sshort-max))
        ((type-case type :ushort) (ushort-max))
        ((type-case type :sint) (sint-max))
        ((type-case type :uint) (uint-max))
        ((type-case type :slong) (slong-max))
        ((type-case type :ulong) (ulong-max))
        ((type-case type :sllong) (sllong-max))
        ((type-case type :ullong) (ullong-max))
        (t (prog2$ (impossible) 0))))

Theorem: integerp-of-integer-type-max

(defthm integerp-of-integer-type-max
  (b* ((min (integer-type-max type)))
    (integerp min))
  :rule-classes :rewrite)

Theorem: integer-type-max-of-type-fix-type

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

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

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