		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Integer-format->signed-min

The ACL2 integer value of the minimum signed value representable in an integer format.

Signature
(integer-format->signed-min format) → min
Arguments: format — Guard (integer-formatp format).
Returns: min — Type (integerp min).

Definitions and Theorems

Function: integer-format->signed-min

(defun integer-format->signed-min (format)
  (declare (xargs :guard (integer-formatp format)))
  (let ((__function__ 'integer-format->signed-min))
    (declare (ignorable __function__))
    (sinteger-format->min (uinteger+sinteger-format->signed
                               (integer-format->pair format)))))

Theorem: integerp-of-integer-format->signed-min

(defthm integerp-of-integer-format->signed-min
  (b* ((min (integer-format->signed-min format)))
    (integerp min))
  :rule-classes :rewrite)

Theorem: integer-format->signed-min-type-prescription

(defthm integer-format->signed-min-type-prescription
  (b* ((common-lisp::?min (integer-format->signed-min format)))
    (and (integerp min) (< min 0)))
  :rule-classes :type-prescription)

Theorem: integer-format->signed-min-lower-bound

(defthm integer-format->signed-min-lower-bound
  (b* ((common-lisp::?min (integer-format->signed-min format)))
    (>= min
        (- (expt 2
                 (1- (integer-format->bit-size format)))))))

Theorem: integer-format->signed-min-of-integer-format-fix-format

(defthm integer-format->signed-min-of-integer-format-fix-format
  (equal (integer-format->signed-min (integer-format-fix format))
         (integer-format->signed-min format)))

Theorem: integer-format->signed-min-integer-format-equiv-congruence-on-format

(defthm
 integer-format->signed-min-integer-format-equiv-congruence-on-format
 (implies (integer-format-equiv format format-equiv)
          (equal (integer-format->signed-min format)
                 (integer-format->signed-min format-equiv)))
 :rule-classes :congruence)