		Search-engine friendly clone of the ACL2 documentation.

Litp

Lit->var

Access the var component of a literal.

Signature
(lit->var lit) → var
Arguments: lit — Guard (litp lit).
Returns: var — Type (varp var).

Definitions and Theorems

Function: lit->var$inline

(defun lit->var$inline (lit)
  (declare (xargs :guard (litp lit)))
  (let ((__function__ 'lit->var))
    (declare (ignorable __function__))
    (ash (the (integer 0 *) (lit-fix lit))
         -1)))

Theorem: varp-of-lit->var

(defthm varp-of-lit->var
  (b* ((var (lit->var$inline lit)))
    (varp var))
  :rule-classes (:rewrite :type-prescription))

Theorem: lit-fix-bound-by-lit->var

(defthm lit-fix-bound-by-lit->var
  (<= (lit-fix x)
      (+ 1 (* 2 (lit->var x))))
  :rule-classes :linear)

Theorem: lit->var$inline-of-lit-fix-lit

(defthm lit->var$inline-of-lit-fix-lit
  (equal (lit->var$inline (lit-fix lit))
         (lit->var$inline lit)))

Theorem: lit->var$inline-lit-equiv-congruence-on-lit

(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)

Subtopics

Lit->var^: Same as lit->var, but with a type declaration that the input is 32 bits unsigned.