restore command will revert the state-stack to its value
present before the put instruction was executed.
substitute for a ``free variable''
Major Section: PROOF-CHECKER-COMMANDS
Example: (put x 17)SubstituteGeneral Form: (put var expr)
expr for the ``free variable'' var, as explained below.
A ``free variable'' is, for our purposes, a variable var such that
the instruction (free var) has been executed earlier in the
state-stack. What (free var) really does is to let var be an
abbreviation for the term (hide var) (see documentation for
add-abbreviation). What (put var expr) really does is to unwind the
state-stack, replacing that free instruction with the instruction
(add-abbreviation var expr), so that future references to (? var)
become reference to expr rather than to (hide var), and then to
replay all the other instructions that were unwound. Because hide
was used, the expectation is that in most cases, the instructions
will replay successfully and put will ``succeed''. However, if any
replayed instruction ``fails'', then the entire replay will abort
and ``fail'', and the state-stack will revert to its value before
the put instruction was executed.
If (put var expr) ``succeeds'', then (remove-abbreviation var) will
be executed at the end.
Note: The restore command will revert the state-stack to its value
present before the put instruction was executed.