Included Books
other
(in-package "ACL2")
include-book
(include-book "def-error-checker")
other
(def-error-checker ensure-value-is-not-in-list ((x "Value to check.") (list true-listp "List that must not include @('x') as member.") (list-description msgp "Description of @('list') for the error message.")) :parents (error-checking) :short "Cause an error if a value is a member of a list." :body (((not (member-equal x list)) "~@0 must not be ~@1, but it is." description list-description)))