F-put-global
Assign to a global variable in state
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.
