`(hons x y)`

returns a normed object equal to `(cons x y)`

.
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.

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.