Included Books
other
(in-package "ACL2")
include-book
(include-book "def-error-checker")
other
(def-error-checker ensure-value-is-boolean ((x "Value to check.")) :parents (error-checking) :short "Cause an error if a value is not a boolean." :body (((booleanp x) "~@0 must be T or NIL, but it is ~x1 instead." description x)))