4vp
Recognizer for four-valued logic constants.
When we are programming and want to refer to a particular logical
value, we generally use (4vx), (4vz), (4vt), and (4vf).
These are just macros that expand to the symbols X, Z, T, and F, in the ACL2
package. We don't write these symbols directly, to try to make it easy to
change their representation if desired.
Definitions and Theorems
Function: 4vp
(defun 4vp (x)
(declare (xargs :guard t))
(or (eq x (4vt))
(eq x (4vf))
(eq x (4vz))
(eq x (4vx))))
