(hons x y) returns a normed object equal to (cons x y).

This documentation topic relates to the experimental extension of ACL2 supporting hash cons, fast alists, and memoization; see hons-and-memoization.

In the logic, hons is just cons; we leave it enabled and would think it odd to ever prove a theorem about it.

Under the hood, hons does whatever is necessary to ensure that its result is normed.

What might this involve?

Since the car and cdr of any normed cons must be normed, we need to hons-copy x and y. This requires little work if x and y are already normed, but can be expensive if x or y contain large, un-normed cons structures.

After that, we need to check whether any normed cons equal to (x . y) already exists. If so, we return it; otherwise, we need to construct a new cons for (x . y) and install it as the normed version of (x . y).

Generally speaking, these extra operations make hons much slower than cons, even when given normed arguments.