next up previous contents
Next: List Scanning Commands Up: Command Reference Previous: Command Reference

Command Line

The interface to the prover is a command line. Each command consists of a command name followed by a number of arguments. The number and type of arguments is determined by the specific command and is never variable. The types of arguments which occur are strings, integers, and terms of the internal language. In the ML interface, string and term arguments are both handled as strings and so enclosed in double quotes; term arguments need special delimiters, as they may include significant spaces. There is a variant command line interface with single letter commands and arguments separated by tabs in the current ML version; it is invoked by the ``walk'' command. Command names in the variant interface can be seen by typing ``h'' in that interface. Another command line interface, very similar to the ML interface, is invoked by the noml command; this uses the same file parser used by the script command.

The standard interface of the current prover is actually the ML interpreter; it is useful to be aware that ML requires all arguments except integers to be enclosed in double quotes, uses tilde for integer negation, requires an argument () for commands with no parameters, and requires that each line end with a semicolon. See the tutorial for examples.

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997