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