Included Books
other
(in-package "ACL2")
include-book
(include-book "std/util/defalist" :dir :system)
other
(defalist symbol-symbollist-alistp (x) :parents (std/typed-alists) :short "Recognize alists from symbols to true lists of symbols." :key (symbolp x) :val (symbol-listp x) :true-listp t :keyp-of-nil t :valp-of-nil t)