Filtering...

alist-defs

books/centaur/misc/alist-defs

Included Books

hons-help hons-extra alist-defuns
other
(in-package "ACL2")
include-book
(include-book "misc/hons-help" :dir :system)
include-book
(include-book "hons-extra")
include-book
(include-book "std/alists/alist-defuns" :dir :system)
hons-acons-eachfunction
(defund hons-acons-each
  (keys val al)
  (declare (xargs :guard t))
  (if (atom keys)
    al
    (hons-acons (car keys)
      val
      (hons-acons-each (cdr keys) val al))))
al-shrinkfunction
(defund al-shrink
  (al)
  (declare (xargs :guard t))
  (hons-shrink-alist al nil))