state
Major Section: ACL2-BUILT-INS
Examples: (f-put-global 'x (expt 2 10) state) (f-put-global 'a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B) state) General Form: (f-put-global (quote symbol) term state)where
symbol is any symbol (with certain enforced exclusions to
avoid overwriting ACL2 system ``globals'') and term is any ACL2
term that could be evaluated at the top-level. F-put-global evaluates
the term, stores the result as the value of the given symbol in the
global-table of state, and returns the new state. (Note: the
actual implementation of the storage of this value is much more
efficient than this discussion of the logic might suggest.)The macro assign is closely related to f-put-global:
(assign var val) macroexpands to (f-put-global 'var val state).
The macros @ and f-get-global give convenient access to the value
of such globals. The :ubt operation has no effect on the
global-table of state. Thus, you may use these globals to hang
onto useful data structures even though you may undo back past where you
computed and saved them.
