|
|
|---|
|
|
|
|---|
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