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.
Logically, hons-equal is merely another name for equal,
i.e., the following is a theorem.
(equal (hons-equal x y) (equal x y))
But 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 eq.