Included Books
other
(in-package "ACL2")
include-book
(include-book "std/typed-alists/string-symbollist-alistp" :dir :system)
include-book
(include-book "std/util/define" :dir :system)
include-book
(include-book "xdoc/constructors" :dir :system)
local
(local (include-book "std/typed-lists/symbol-listp" :dir :system))
other
(define organize-symbols-by-name ((syms symbol-listp)) :returns (syms-by-name string-symbollist-alistp :hyp :guard) :parents (std/basic) :short "Organize a list of symbols by their names." :long (topstring (p "The result is an alist from symbol names (strings) to the non-empty lists of the symbols that have the respective names.") (p "The alist has unique keys, and each of its values has no duplicates.")) (organize-symbols-by-name-aux syms nil) :prepwork ((define organize-symbols-by-name-aux ((syms symbol-listp) (acc string-symbollist-alistp)) :returns (syms-by-name string-symbollist-alistp :hyp :guard) :parents nil (b* (((when (endp syms)) acc) (sym (car syms)) (name (symbol-name sym)) (prev-syms-for-name (cdr (assoc-equal name acc)))) (organize-symbols-by-name-aux (cdr syms) (put-assoc-equal name (add-to-set-eq sym prev-syms-for-name) acc))))))