## INSTRUCTIONS

instructions to the proof checker
Major Section: PROOF-CHECKER

Example:
:instructions (induct prove promote (dive 1) x
(dive 2) = top (drop 2) prove)

See defthm for the role of `:instructions`

in place of
`:`

`hints`

. As illustrated by the example above, the value
associated with `:instructions`

is a list of proof-checker
commands. At the moment the best way to understand the idea of the
interactive proof-checker (see proof-checker and
see verify) is probably to read the first 11 pages of CLI
Technical Report 19, which describes the corresponding facility for
Nqthm.

When inside the interactive loop (i.e., after executing `verify`

),
use `help`

to get a list of legal instructions and `(help instr)`

to get help for the instruction `instr`

.