(fast-alist-len alist) counts the number of unique keys in a fast alist.

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.