		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Char-format->max

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

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

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

Definitions and Theorems

Function: char-format->max

(defun char-format->max (char-format uchar-format schar-format)
  (declare (xargs :guard (and (char-formatp char-format)
                              (uchar-formatp uchar-format)
                              (schar-formatp schar-format))))
  (let ((__function__ 'char-format->max))
    (declare (ignorable __function__))
    (if (char-format->signedp char-format)
        (schar-format->max schar-format uchar-format)
      (uchar-format->max uchar-format))))

Theorem: posp-of-char-format->max

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

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

(defthm char-format->max-type-prescription
  (b*
    ((common-lisp::?max
          (char-format->max char-format uchar-format schar-format)))
    (and (posp max) (> max 1)))
  :rule-classes :type-prescription)

Theorem: char-format->max-lower-bound

(defthm char-format->max-lower-bound
  (b*
    ((common-lisp::?max
          (char-format->max char-format uchar-format schar-format)))
    (>= max 127))
  :rule-classes :linear)

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

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

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

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

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

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

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

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

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

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

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

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