		Search-engine friendly clone of the ACL2 documentation.

Integer-operations

Value-integer-and-value-integer->get

Theorems about value-integer and value-integer->get.

Definitions and Theorems

Theorem: value-integer-of-value-integer->get-when-type-of-value

(defthm value-integer-of-value-integer->get-when-type-of-value
  (implies (and (value-integerp val)
                (equal type (type-of-value val)))
           (equal (value-integer (value-integer->get val)
                                 type)
                  (value-fix val))))

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

(defthm value-integer->get-of-value-integer
  (b* ((val (value-integer mathint type)))
    (implies (and (type-nonchar-integerp type)
                  (integer-type-rangep mathint type))
             (equal (value-integer->get val)
                    (ifix mathint)))))