		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)