Major Section: OTHER
Examples: (assign x (expt 2 10)) (assign a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B))where
General Form: (assign symbol term)
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 term state) state)).The macro
@gives convenient access to the value of such globals. The
ubtoperation has no effect on the
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.