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