		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Ienv-sint-rangep

Check if an ACl2 integer is in the range of (i.e. representable in) type signed int.

Signature
(ienv-sint-rangep val ienv) → yes/no
Arguments: val — Guard (integerp val).; ienv — Guard (ienvp ienv).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: ienv-sint-rangep

(defun ienv-sint-rangep (val ienv)
  (declare (xargs :guard (and (integerp val) (ienvp ienv))))
  (and (<= (ienv->sint-min ienv) (ifix val))
       (<= (ifix val) (ienv->sint-max ienv))))

Theorem: booleanp-of-ienv-sint-rangep

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

Theorem: ienv-sint-rangep-correct

(defthm ienv-sint-rangep-correct
  (equal (ienv-sint-rangep val ienv)
         (c::ienv-sint-rangep val (ldm-ienv ienv))))

Theorem: ienv-sint-rangep-of-ifix-val

(defthm ienv-sint-rangep-of-ifix-val
  (equal (ienv-sint-rangep (ifix val) ienv)
         (ienv-sint-rangep val ienv)))

Theorem: ienv-sint-rangep-int-equiv-congruence-on-val

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

Theorem: ienv-sint-rangep-of-ienv-fix-ienv

(defthm ienv-sint-rangep-of-ienv-fix-ienv
  (equal (ienv-sint-rangep val (ienv-fix ienv))
         (ienv-sint-rangep val ienv)))

Theorem: ienv-sint-rangep-ienv-equiv-congruence-on-ienv

(defthm ienv-sint-rangep-ienv-equiv-congruence-on-ienv
  (implies (ienv-equiv ienv ienv-equiv)
           (equal (ienv-sint-rangep val ienv)
                  (ienv-sint-rangep val ienv-equiv)))
  :rule-classes :congruence)