		Search-engine friendly clone of the ACL2 documentation.

Values

Int-value-to-int

ACL2 integer value corresponding to a Leo integer value.

Signature
(int-value-to-int x) → int
Arguments: x — Guard (int-valuep x).
Returns: int — Type (integerp int).

Definitions and Theorems

Function: int-value-to-int

(defun int-value-to-int (x)
  (declare (xargs :guard (int-valuep x)))
  (let ((__function__ 'int-value-to-int))
    (declare (ignorable __function__))
    (case (value-kind x)
      (:u8 (value-u8->get x))
      (:u16 (value-u16->get x))
      (:u32 (value-u32->get x))
      (:u64 (value-u64->get x))
      (:u128 (value-u128->get x))
      (:i8 (value-i8->get x))
      (:i16 (value-i16->get x))
      (:i32 (value-i32->get x))
      (:i64 (value-i64->get x))
      (:i128 (value-i128->get x))
      (t (prog2$ (impossible) 0)))))

Theorem: integerp-of-int-value-to-int

(defthm integerp-of-int-value-to-int
  (b* ((int (int-value-to-int x)))
    (integerp int))
  :rule-classes :rewrite)

Theorem: int-value-to-int-of-value-fix-x

(defthm int-value-to-int-of-value-fix-x
  (equal (int-value-to-int (value-fix x))
         (int-value-to-int x)))

Theorem: int-value-to-int-value-equiv-congruence-on-x

(defthm int-value-to-int-value-equiv-congruence-on-x
  (implies (value-equiv x x-equiv)
           (equal (int-value-to-int x)
                  (int-value-to-int x-equiv)))
  :rule-classes :congruence)