push a temporary, new environment for hash consing

This documentation topic relates to an experimental extension of ACL2 under development by Bob Boyer and Warren Hunt. See hons-and-memoization.

The value of (hons-let form) is the same as the value of form. However, in the former case a new hons environment is temporarily created, where no hash conses are stored. The pre-existing hons environment is restored upon exit from the evaluation of a hons-let expression.

We may write more on this topic, especially upon request.