		Search-engine friendly clone of the ACL2 documentation.

Booleanp

Recognizer for booleans

(Booleanp x) is t if x is t or nil, and is nil otherwise.

See generalized-booleans for a discussion of a potential soundness problem for ACL2 related to the question: Which Common Lisp functions are known to return Boolean values?

Function: booleanp

(defun booleanp (x)
  (declare (xargs :guard t))
  (if (eq x t) t (eq x nil)))

Subtopics

Boolean-listp: Recognizer for a true list of booleans
Bool-fix: (bool-fix x) is a fixing function for Booleans; it coerces any non-nil symbol to t.