		Search-engine friendly clone of the ACL2 documentation.

Values

Value-rational->get

Return the ACL2 rational from its meta representation.

Signature
(value-rational->get x) → x-rational
Arguments: x — Guard (and (valuep x) (value-case-rational x)).
Returns: x-rational — Type (rationalp x-rational).

The name of this function is analogous to the accessor value-number->get of the fixtype of values.

Definitions and Theorems

Function: value-rational->get

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

Theorem: rationalp-of-value-rational->get

(defthm rationalp-of-value-rational->get
        (b* ((x-rational (value-rational->get x)))
            (rationalp x-rational))
        :rule-classes :rewrite)

Theorem: value-rational->get-of-value-fix-x

(defthm value-rational->get-of-value-fix-x
        (equal (value-rational->get (value-fix x))
               (value-rational->get x)))

Theorem: value-rational->get-value-equiv-congruence-on-x

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