		Search-engine friendly clone of the ACL2 documentation.

Logops-bit-functions

B-ite

If-then-else for bitps.

Signature
(b-ite test then else) → bit
Arguments: test — Guard (bitp test).; then — Guard (bitp then).; else — Guard (bitp else).
Returns: bit — Type (bitp bit).

Definitions and Theorems

Function: b-ite$inline

(defun b-ite$inline (test then else)
  (declare (xargs :guard (and (bitp test)
                              (bitp then)
                              (bitp else))))
  (let ((__function__ 'b-ite))
    (declare (ignorable __function__))
    (if (zbp test)
        (bfix else)
      (bfix then))))

Theorem: bitp-of-b-ite

(defthm bitp-of-b-ite
  (b* ((bit (b-ite$inline test then else)))
    (bitp bit))
  :rule-classes :type-prescription)