(hons-equal x y) is a recursive equality check that optimizes when parts of its arguments are normed.

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-equal is just equal; we leave it enabled and would think it odd to ever prove a theorem about it.

Under the hood, when hons-equal encounters two arguments that are both normed, it becomes a mere eql check, and hence avoids the overhead of recursively checking large cons structures for equality.

Note. If hons-equal is given arguments that do not contain many normed objects, it can actually be much slower than equal! This is because it checks to see whether its arguments are normed at each recursive step, and so you are repeatedly paying the price of such checks. Also see hons-equal-lite, which only checks at the top level whether its arguments are normed.