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 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.