WITH-LOCAL-STOBJ

locally bind a single-threaded object 
Major Section:  STOBJ

See stobj for an introduction to single-threaded objects. 

Example Form:
(with-local-stobj
 st
 (mv-let (result st)
         (compute-with-st x st)
         result))
With-local-stobj can be thought of as a macro, where the example form above expands as follows. 
(mv-let (result st)
        (let ((st (create-st)))
          (compute-with-st x st))
        (declare (ignore st))
        result)
However, ACL2 expects you to use with-local-stobj, not its expansion. More precisely, stobj creator functions are not allowed except (implicitly) via with-local-stobj and in logic-only situations (like theorems and hints). Moreover, neither with-local-stobj nor its expansions are legal when typed directly at the top-level loop. 

General Forms:
(with-local-stobj stobj-name mv-let-form)
(with-local-stobj stobj-name mv-let-form creator-name)
where stobj-name is the name of a stobj other than state, mv-let-form is a call of mv-let, and if creator-name is supplied then it should be the name of the creator function for stobj-name; see defstobj. For the example form above, its expansion would use creator-name, if supplied, in place of create-st.

With-local-stobj can be useful when a stobj is used to memoize intermediate results during a computation, yet it is desired not to make the stobj a formal parameter for the function and its callers.

ACL2 can reason about these ``local stobjs,'' and in particular about stobj creator functions. For technical reasons, ACL2 will not allow you to enable the :EXECUTABLE-COUNTERPART rune of a stobj creator function.