Major Section: HONS-AND-MEMOIZATION
This documentation topic relates to the experimental extension of ACL2 supporting hash cons, fast alists, and memoization; see hons-and-memoization.
Logically, this function just returns
nil. But execution of
(never-memoize fn) records that
fn must never be memoized, so that
any attempt to memoize
fn will fail.
Any function can be marked as unsafe to memoize; in fact,
fn need not
even be defined at the time it is marked.
This is useful for prohibiting the memoization of functions that are known to
involve destructive functions like