Hons-equal-lite
(hons-equal-lite x y) is a non-recursive equality check that
optimizes if its arguments are normed.
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.
Function: hons-equal-lite
(defun hons-equal-lite (x y)
(declare (xargs :guard t))
(equal x y))
