assign to a global variable in state
Major Section:  ACL2-BUILT-INS

(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.