@

get the value of a global variable in state 
Major Section:  ACL2-BUILT-INS


Examples:
(+ (@ y) 1)
(assign a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B))

General Form:
(@ symbol)
where symbol is 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.

The macro f-get-global is closely related to @: (@ var) macroexpands to (f-get-global 'var state).

The macro assign 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.