Major Section: ACL2-BUILT-INS
Examples: (+ (@ y) 1) (assign a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B)) General Form: (@ symbol)where
symbolis any symbol to which you have
assigned a global value. This macro expands into
(f-get-global 'symbol state), which retrieves the stored value of the symbol.
f-get-global is closely related to
(f-get-global 'var state).
assign makes it convenient to set the value of a symbol.
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