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-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 x and
(hons-copy x) are definitely equal. But ACL2 will not
permit you to call eq on them because the guard for eq is
(or (symbolp x) (symbolp y)).