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