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
symbolis any symbol (with certain enforced exclusions to avoid overwriting ACL2 system ``globals'') and
termis any ACL2 term that could be evaluated at the top-level.
Assignevaluates the term, stores the result as the value of the given symbol in the
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.)
Assignis 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)).
f-put-global is closely related to
(assign var val) macroexpands to
(f-put-global 'var val state).
@ gives convenient access to the value of such globals.
ubt operation has no effect on the
Thus, you may use these globals to hang onto useful data structures
even though you may undo back past where you computed and saved