Included Books
other
(in-package "ACL2")
include-book
(include-book "def-error-checker")
other
(def-error-checker ensure-list-has-no-duplicates ((list true-listp "List to check.")) :parents (error-checking) :short "Cause an error if a list has duplicates." :body (((no-duplicatesp-equal list) "~@0 must have no duplicates." description)))