		Search-engine friendly clone of the ACL2 documentation.

Logops-definitions

Logite

Bitwise if-then-else among integers.

Signature
(logite test then else) → logite
Returns: logite — Type (integerp logite).

Definitions and Theorems

Function: logite

(defun logite (test then else)
  (declare (type integer test)
           (type integer then)
           (type integer else))
  (let ((__function__ 'logite))
    (declare (ignorable __function__))
    (logior (logand test then)
            (logand (lognot test) else))))

Theorem: logite-type

(defthm logite-type
  (b* ((logite (logite test then else)))
    (integerp logite))
  :rule-classes :type-prescription)

Subtopics

Ihs/logite-lemmas: Lemmas about logite from the logops-lemmas book.