		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

Bool->vec

Convert an ACL2 booleanp into a 4vec according to the boolean-convention.

Signature
(bool->vec x) → *
Arguments: x — Guard (booleanp x).

Definitions and Theorems

Function: bool->vec$inline

(defun bool->vec$inline (x)
  (declare (xargs :guard (booleanp x)))
  (let ((__function__ 'bool->vec))
    (declare (ignorable __function__))
    (if x -1 0)))

Theorem: bool->vec-cases

(defthm bool->vec-cases
  (and (implies x (equal (bool->vec x) -1))
       (implies (not x)
                (equal (bool->vec x) 0))))