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

the missing argument, for example, =>, normalization
a carriage return, which aborts execution of the command

a question mark, which provides help such as

Legal display modes:
  qualified    unambiguous  unqualified

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.