		Search-engine friendly clone of the ACL2 documentation.

Litp

Lit->neg

Access the neg bit of a literal.

Signature
(lit->neg lit) → neg
Arguments: lit — Guard (litp lit).
Returns: neg — Type (bitp neg).

Definitions and Theorems

Function: lit->neg$inline

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

Theorem: bitp-of-lit->neg

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

Theorem: natp-of-lit->neg

(defthm natp-of-lit->neg
  (natp (lit->neg lit))
  :rule-classes (:type-prescription :tau-system))

Theorem: lit->neg-bound

(defthm lit->neg-bound
  (<= (lit->neg lit) 1)
  :rule-classes :linear)

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

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

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

(defthm lit->neg$inline-lit-equiv-congruence-on-lit
  (implies (lit-equiv lit lit-equiv)
           (equal (lit->neg$inline lit)
                  (lit->neg$inline lit-equiv)))
  :rule-classes :congruence)

Subtopics

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