(hons-get key alist) is the efficient lookup operation for fast-alists.

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.