		Search-engine friendly clone of the ACL2 documentation.

Values

Value-case-integer

Check if a value is an integer.

Signature
(value-case-integer x) → yes/no
Arguments: x — Guard (valuep x).
Returns: yes/no — Type (booleanp yes/no).

The name of this function is analogous to the notation (value-case ... :number) of the fixtype of values.

Definitions and Theorems

Function: value-case-integer

(defun value-case-integer (x)
  (declare (xargs :guard (valuep x)))
  (let ((__function__ 'value-case-integer))
    (declare (ignorable __function__))
    (and (value-case x :number)
         (integerp (value-number->get x)))))

Theorem: booleanp-of-value-case-integer

(defthm booleanp-of-value-case-integer
  (b* ((yes/no (value-case-integer x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: value-case-integer-of-value-fix-x

(defthm value-case-integer-of-value-fix-x
  (equal (value-case-integer (value-fix x))
         (value-case-integer x)))

Theorem: value-case-integer-value-equiv-congruence-on-x

(defthm value-case-integer-value-equiv-congruence-on-x
  (implies (value-equiv x x-equiv)
           (equal (value-case-integer x)
                  (value-case-integer x-equiv)))
  :rule-classes :congruence)