Allow the use of STATE as a formal parameter
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so
In brief: The variable symbol state has an unusual status in ACL2.
In order to use it, you either need to issue :set-state-ok t, as we
explain below, or you need to declare it to be a stobj, as explained
elsewhere (see declare-stobjs). Now we explain in more detail.
Because the variable symbol state denotes the ``current ACL2
state,'' ACL2 treats the symbol very restrictively when it occurs as a formal
parameter of a defined function. The novice user, who is unlikely to be aware
of the special status of that symbol, is likely to be confused when error
messages about STATE are printed in response to the innocent choice of
that symbol as a formal variable. Therefore the top-level ACL2 loop can
operate in a mode in which state is simply disallowed as a formal
For a discussion of STATE, See state and see stobj.
Roughly speaking, at the top-level, the ``current ACL2 state'' is denoted by
the variable symbol STATE. Only the current state may be passed into a
function expecting a state as an argument. Furthermore, the name of the
formal parameter into which the current state is passed must be STATE and
nothing but the current state may be passed into a formal of that name.
Therefore, only certain access and change functions can use that formal
— namely those with a STATE formal — and if any such function
produces a new state it becomes the ``current state'' and must be passed along
in the STATE position thereafter. Thus, ACL2 requires that the state be
single-threaded. This, in turn, allows us to represent only one state at a
time and to produce new states from it destructively in a von Neumannesque
fashion. The syntactic restrictions on the variable STATE are enforced
by the translate mechanism (see trans and see term) when terms
To prevent the novice user from seeing messages prohibiting certain uses of
the variable symbol STATE ACL2 has a mode in which it simply disallows
the use of that symbol as a formal parameter. Use of the symbol causes a
simple error message. The system is initially in that mode.
To get out of that mode, execute:
:set-state-ok t ;;; or, (set-state-ok t)
It is not recommended that you do this until you have read the
documentation of state.
To enter the mode in which use of state is prohibited as a formal
The mode is stored in the defaults table, See ACL2-defaults-table.
Thus, the mode may be set locally in books.