equality for hons pairs
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.