(hons-get key alist)is the efficient lookup operation for
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.
hons-get is just an alias for
typically leave it enabled and prefer to reason about
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
hons-get first norms
gethash operation on the hidden hash table.