NEVER-MEMOIZE

Mark a function as unsafe to memoize.
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 nreverse.