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