		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Svex-int

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

Definitions and Theorems

Function: svex-int$inline

(defun svex-int$inline (x)
  (declare (xargs :guard (integerp x)))
  (let ((__function__ 'svex-int))
    (declare (ignorable __function__))
    (svex-quote (2vec (lifix x)))))

Theorem: svex-p-of-svex-int

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

Theorem: svex-int-correct

(defthm svex-int-correct
  (b* ((?svex (svex-int$inline x)))
    (equal (svex-eval svex env)
           (2vec (ifix x)))))

Theorem: svex-int-vars

(defthm svex-int-vars
  (b* nil
    (equal (svex-vars (svex-int x)) nil)))

Theorem: svex-int$inline-of-ifix-x

(defthm svex-int$inline-of-ifix-x
  (equal (svex-int$inline (ifix x))
         (svex-int$inline x)))

Theorem: svex-int$inline-int-equiv-congruence-on-x

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