identity function that creates 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-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)).