Major Section: ACL2-BUILT-INS
Examples: (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
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.
F-put-globalevaluates the term, stores the result as the value of the given symbol in the
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.)
assign is closely related to
(assign var val) macroexpands to
(f-put-global 'var val state).
f-get-global give convenient access to the value
of such globals. The
ubt operation 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.