		Search-engine friendly clone of the ACL2 documentation.

Values

Value-case-rational

Check if a value is a rational.

Signature
(value-case-rational 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-rational

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

Theorem: booleanp-of-value-case-rational

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

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

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

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

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