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