(hons-get key alist)
is the efficient lookup operation for
fast-alists.
Major Section: HONS-AND-MEMOIZATION
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.