		Search-engine friendly clone of the ACL2 documentation.

Integer-ranges

Integer-type-min

Minimum mathematical integer value of an integer type.

Signature
(integer-type-min 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-min

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

Theorem: integerp-of-integer-type-min

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

Theorem: integer-type-min-of-type-fix-type

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

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

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