Hons-get
(hons-get key alist) is the efficient lookup operation for fast-alists.
Logically, hons-get is just an alias for hons-assoc-equal; we typically leave it enabled and prefer to reason about
hons-assoc-equal instead. One benefit of this approach is that it helps
to avoids "false" discipline warnings that might arise from execution during
theorem proving.
Under the hood, when alist is a fast alist that is associated with a
valid hash table, hons-get first norms key using hons-copy,
then becomes a gethash operation on the hidden hash table. Otherwise
hons-get simply invokes hons-assoc-equal, which is similar (in
definition and in performance) to assoc-equal, on key and
alist.
Function: hons-get
(defun hons-get (key alist)
(declare (xargs :guard t))
(hons-assoc-equal key alist))
Subtopics
- Std/alists/hons-assoc-equal
- Lemmas about hons-assoc-equal available in the std/alists library.
