Same as lit->var, but with a type declaration that the input is 32 bits unsigned.
(lit->var^ lit) → *
Function:
(defun lit->var^$inline (lit) (declare (type (unsigned-byte 32) lit)) (declare (xargs :guard (litp lit))) (let ((__function__ 'lit->var^)) (declare (ignorable __function__)) (mbe :logic (lit->var lit) :exec (the (unsigned-byte 31) (ash (the (unsigned-byte 32) lit) -1)))))
Theorem:
(defthm lit->var^$inline-of-lit-fix-lit (equal (lit->var^$inline (lit-fix lit)) (lit->var^$inline lit)))
Theorem:
(defthm lit->var^$inline-lit-equiv-congruence-on-lit (implies (lit-equiv lit lit-equiv) (equal (lit->var^$inline lit) (lit->var^$inline lit-equiv))) :rule-classes :congruence)