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