F-GET-GLOBAL

get the value of a global variable in 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.