Free Variables in Top-Level Input

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)

There is an exception to this 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 @ .