(hons-get key alist) is the efficient lookup operation for
fast-alists.
Major Section: HONS-AND-MEMOIZATION
This documentation topic relates to the experimental extension of ACL2 supporting hash cons, fast alists, and memoization; see 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.
