`(hons-equal-lite x y)`

is a non-recursive equality check that optimizes if
` `

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-lite`

is just `equal`

; we leave it enabled and
would think it odd to ever prove a theorem about it.

Under the hood, `hons-equal-lite`

checks whether its arguments are normed,
and if so it effectively becomes a `eql`

check. Otherwise, it immediately
calls `equal`

to determine if its arguments are equal.

The idea here is to strike a useful balance between `equal`

and
`hons-equal`

. If both arguments happen to be normed, we get to use a very
fast equality comparison. Otherwise, we just get out of the way and let
`equal`

do its work, without the extra overhead of recursively checking
whether the subtrees of x and y are normed.