		Search-engine friendly clone of the ACL2 documentation.

Values

Value-integer->get

Return the ACL2 integer from its meta representation.

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

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

Definitions and Theorems

Function: value-integer->get

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

Theorem: integerp-of-value-integer->get

(defthm integerp-of-value-integer->get
  (b* ((x-integer (value-integer->get x)))
    (integerp x-integer))
  :rule-classes :rewrite)

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

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

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

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