state
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 symbol is any symbol to which you have assigned a global
value.The macro @ is closely related to f-get-global: (@ var)
macroexpands to (f-get-global 'var state).
The macro f-get-global makes it convenient to set the value of a
symbol. The :ubt operation has no effect on the global-table
of 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.
