ACL2 !>(equal (app (app a b) c)
(app a (app b c))))
ACL2 Error in TOP-LEVEL: Global variables, such as C, B, and A, are
not allowed. See :DOC ASSIGN and :DOC @.
ACL2 does not allow ``global variables'' in top-level input. There is no ``top-level binding environment'' to give meaning to these variables.
Thus, expressions involving no variables can generally be evaluated,
ACL2 !>(equal (app (app '(1 2) '(3 4)) '(5 6))
(app '(1 2) (app '(3 4) '(5 6))))
(1 2 3 4 5 6)
but expressions containing variables cannot.
There is an exception to rule. References to ``single-threaded
objects'' may appear in top-level forms. See stobj 
. A
single-threaded object is an ACL2 object, usually containing many
fields, whose use is syntactically restricted so that it may be
given as input only to certain functions and must be returned as
output by certain functions. These restrictions allow single-
threaded objects to be efficiently manipulated. For example, only a
single copy of the object actually exists, even though from a
logical perspective one might expect the object to be ``copied on
write.''
The most commonly used single-threaded object in ACL2 is the ACL2
system state, whose current value is always held in the variable
state .
ACL2 provides a way for you to use state to save values of
computations at the top-level and refer to them later. See
assign and @ .
