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-copy is merely another name for the
identity function, i.e., the following is a theorem.
(equal (hons-copy x) x)
Hons-copy returns a value in which all conses are honses.
You cannot directly tell this from within ACL2, where both
(hons-copy x) are definitely
equal. But ACL2 will not
permit you to call
eq on them because the guard for
(or (symbolp x) (symbolp y)).