Hons-assoc-equal
(hons-assoc-equal key alist) is not fast; it serves as
the logical definition for hons-get.
The definition of hons-assoc-equal is similar to that of
assoc-equal, except that (1) it does not require alistp as a
guard, and (2) it "skips over" any non-conses when its alist argument is
malformed.
We typically leave hons-get enabled and reason about
hons-assoc-equal instead. One benefit of this approach is that it avoids
certain "false" discipline warnings that might arise from execution during
theorem proving.
Function: hons-assoc-equal
(defun hons-assoc-equal (key alist)
(declare (xargs :guard t))
(cond ((atom alist) nil)
((and (consp (car alist))
(hons-equal key (caar alist)))
(car alist))
(t (hons-assoc-equal key (cdr alist)))))Subtopics
- Std/alists/hons-assoc-equal
- Lemmas about hons-assoc-equal available in the std/alists library.
