		Search-engine friendly clone of the ACL2 documentation.

Sparseint

Int-to-sparseint

Convert an integer into a sparseint.

Signature
(int-to-sparseint x) → sint
Arguments: x — Guard (integerp x).
Returns: sint — Type (sparseint-p sint).

Definitions and Theorems

Function: int-to-sparseint$inline

(defun int-to-sparseint$inline (x)
  (declare (xargs :guard (integerp x)))
  (let ((__function__ 'int-to-sparseint))
    (declare (ignorable __function__))
    (int-to-sparseint$ x)))

Theorem: sparseint-p-of-int-to-sparseint

(defthm sparseint-p-of-int-to-sparseint
  (b* ((sint (int-to-sparseint$inline x)))
    (sparseint-p sint))
  :rule-classes :rewrite)

Theorem: sparseint-val-of-int-to-sparseint

(defthm sparseint-val-of-int-to-sparseint
  (b* ((?sint (int-to-sparseint$inline x)))
    (equal (sparseint-val sint) (ifix x))))

Theorem: int-to-sparseint$inline-of-ifix-x

(defthm int-to-sparseint$inline-of-ifix-x
  (equal (int-to-sparseint$inline (ifix x))
         (int-to-sparseint$inline x)))

Theorem: int-to-sparseint$inline-int-equiv-congruence-on-x

(defthm int-to-sparseint$inline-int-equiv-congruence-on-x
  (implies (int-equiv x x-equiv)
           (equal (int-to-sparseint$inline x)
                  (int-to-sparseint$inline x-equiv)))
  :rule-classes :congruence)