Major Section: HONS
This documentation topic relates to an experimental extension of ACL2 under development by Bob Boyer and Warren Hunt. See hons-and-memoization.
hons-equal is merely another name for
i.e., the following is a theorem.
(equal (hons-equal x y) (equal x y))
hons-equal may run much faster than
equal in some
cases. If both arguments are determined to be honses, then
hons-equal becomes a mere