LP, the Larch Prover -- Command arguments


Many commands take one or more arguments. If you know how to use a command, you can type its arguments on the same line as the command. If you don't, LP will prompt you for the arguments. For example, you can type an entire command
set display-mode
in response to LP's command prompt, or you can type an abbreviation of the command without any arguments and await a further prompt:
LP1: set display

The current display-mode is `unambiguous'.

New display-mode:
In response to this prompt, you can type

Commands that require a possibly lengthy argument allow you to enter it on more than one line. To do this, don't type the argument on the command line; instead, type it on the following lines, terminating your input with a line consisting of two periods (..). For example,

LP1: declare sort Nat

LP2: declare operators
Please enter operator declarations, terminated with a `..' line, or `?' for
help:
0: -> Nat
s: Nat -> Nat
..
If you need help in the middle of typing a lengthy argument, type a question mark on a line by itself.