ASSIGN

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


Examples:
(assign x (expt 2 10))
(assign a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B))

General Form:
(assign symbol term)
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. Assign evaluates the term, stores the result as the value of the given symbol in the global-table of state, and returns the result. (Note: the actual implementation of the storage of this value is much more efficient than this discussion of the logic might suggest.) Assign is a macro that effectively expands to the more complicated but understandable: 
(pprogn (f-put-global 'symbol term state)
        (mv nil (f-get-global 'symbol state) state)).

The macro f-put-global is closely related to assign: (assign var val) macroexpands to (f-put-global 'var val state).

The macro @ gives 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.