(hons-equal x y) is a recursive equality check that optimizes when parts of
its arguments are normed.
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-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.
