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