(fast-alist-len alist)
counts the number of unique keys in a fast alist.
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 this function counts how many elements would remain in the alist were
we to shrink it with hons-shrink-alist
.
Good discipline requires that the alist is a fast alist. Under the hood, when
the alist is a fast alist we can simply call the underlying Common Lisp
function hash-table-count
on the associated hash table, which is very fast
and doesn't require us to actually shrink the alist.