		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Schar-rangep

Check if a mathematical integer is in the range of (i.e. representable in) type signed char.

Signature
(schar-rangep val) → yes/no
Arguments: val — Guard (integerp val).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: schar-rangep

(defun schar-rangep (val)
  (declare (xargs :guard (integerp val)))
  (let ((__function__ 'schar-rangep))
    (declare (ignorable __function__))
    (and (<= (schar-min) (ifix val))
         (<= (ifix val) (schar-max)))))

Theorem: booleanp-of-schar-rangep

(defthm booleanp-of-schar-rangep
  (b* ((yes/no (schar-rangep val)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: schar-rangep-of-ifix-val

(defthm schar-rangep-of-ifix-val
  (equal (schar-rangep (ifix val))
         (schar-rangep val)))

Theorem: schar-rangep-int-equiv-congruence-on-val

(defthm schar-rangep-int-equiv-congruence-on-val
  (implies (acl2::int-equiv val val-equiv)
           (equal (schar-rangep val)
                  (schar-rangep val-equiv)))
  :rule-classes :congruence)