Major Section: HONS-AND-MEMOIZATION
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
However, in the former case a new
hons environment is temporarily
created, where no hash conses are stored. The pre-existing
environment is restored upon exit from the evaluation of a
We may write more on this topic, especially upon request.