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)
but expressions containing variables cannot.
There is an exception to this rule. References to ``single-threaded
objects'' may appear in top-level forms. See stobj
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