		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Integer-format->signed-max

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

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

Definitions and Theorems

Function: integer-format->signed-max

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

Theorem: posp-of-integer-format->signed-max

(defthm posp-of-integer-format->signed-max
  (b* ((max (integer-format->signed-max format)))
    (posp max))
  :rule-classes (:rewrite :type-prescription))

Theorem: integer-format->signed-max-upper-bound

(defthm integer-format->signed-max-upper-bound
  (b* ((common-lisp::?max (integer-format->signed-max format)))
    (<= max
        (1- (expt 2
                  (1- (integer-format->bit-size format))))))
  :rule-classes :linear)

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

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

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

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