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