allow a reference to state in raw Lisp
Major Section:  PROGRAMMING

Example Form:
(with-live-state (assign y 3))

General form: (with-live-state form)

where form is an arbitrary form that mentions state.

Most users will not need with-live-state. If for some reason a form that mentions the variable state might be executed in raw Lisp, outside the ACL2 loop, then the use of with-live-state is recommended in order to avoid potential warnings or (less likely) errors.