		Search-engine friendly clone of the ACL2 documentation.

Char-formats

Char-format->min

The ACL2 integer value of CHAR_MIN [C17:5.2.4.2.1/1].

Signature
(char-format->min char-format uchar-format schar-format) → min
Arguments: char-format — Guard (char-formatp char-format).; uchar-format — Guard (uchar-formatp uchar-format).; schar-format — Guard (schar-formatp schar-format).
Returns: min — Type (integerp min).

As explained in [C17:5.2.4.2.1/2], this is either 0 or the same as SCHAR_MIN.

Definitions and Theorems

Function: char-format->min

(defun char-format->min (char-format uchar-format schar-format)
  (declare (xargs :guard (and (char-formatp char-format)
                              (uchar-formatp uchar-format)
                              (schar-formatp schar-format))))
  (if (char-format->signedp char-format)
      (schar-format->min schar-format uchar-format)
    0))

Theorem: integerp-of-char-format->min

(defthm integerp-of-char-format->min
  (b*
    ((min (char-format->min char-format uchar-format schar-format)))
    (integerp min))
  :rule-classes :rewrite)

Theorem: char-format->min-type-prescription

(defthm char-format->min-type-prescription
  (b*
    ((common-lisp::?min
          (char-format->min char-format uchar-format schar-format)))
    (and (integerp min) (<= min 0)))
  :rule-classes :type-prescription)

Theorem: char-format->min-upper-bound

(defthm char-format->min-upper-bound
 (b*
   ((common-lisp::?min
         (char-format->min char-format uchar-format schar-format)))
   (<= min 0))
 :rule-classes
 ((:linear
    :trigger-terms ((char-format->min char-format
                                      uchar-format schar-format)))))

Theorem: char-format->min-of-char-format-fix-char-format

(defthm char-format->min-of-char-format-fix-char-format
  (equal (char-format->min (char-format-fix char-format)
                           uchar-format schar-format)
         (char-format->min char-format uchar-format schar-format)))

Theorem: char-format->min-char-format-equiv-congruence-on-char-format

(defthm char-format->min-char-format-equiv-congruence-on-char-format
 (implies
     (char-format-equiv char-format char-format-equiv)
     (equal (char-format->min char-format uchar-format schar-format)
            (char-format->min char-format-equiv
                              uchar-format schar-format)))
 :rule-classes :congruence)

Theorem: char-format->min-of-uchar-format-fix-uchar-format

(defthm char-format->min-of-uchar-format-fix-uchar-format
  (equal (char-format->min char-format
                           (uchar-format-fix uchar-format)
                           schar-format)
         (char-format->min char-format uchar-format schar-format)))

Theorem: char-format->min-uchar-format-equiv-congruence-on-uchar-format

(defthm
     char-format->min-uchar-format-equiv-congruence-on-uchar-format
 (implies
     (uchar-format-equiv uchar-format uchar-format-equiv)
     (equal (char-format->min char-format uchar-format schar-format)
            (char-format->min char-format
                              uchar-format-equiv schar-format)))
 :rule-classes :congruence)

Theorem: char-format->min-of-schar-format-fix-schar-format

(defthm char-format->min-of-schar-format-fix-schar-format
  (equal (char-format->min char-format uchar-format
                           (schar-format-fix schar-format))
         (char-format->min char-format uchar-format schar-format)))

Theorem: char-format->min-schar-format-equiv-congruence-on-schar-format

(defthm
     char-format->min-schar-format-equiv-congruence-on-schar-format
 (implies
     (schar-format-equiv schar-format schar-format-equiv)
     (equal (char-format->min char-format uchar-format schar-format)
            (char-format->min char-format
                              uchar-format schar-format-equiv)))
 :rule-classes :congruence)