LP, the Larch Prover — Abbreviations for commands

LP allows users to abbreviate a command with an unambiguous prefix of that command. For example, the declare command can be abbreviated to dec, but not to de because de is also a prefix of the delete command.

LP also allows users to abbreviate certain command arguments with unambiguous prefixes. When the argument can be a hyphenated word, it is enough to supply unambiguous prefixes of the hyphenated components. Examples:

Command                              Abbreviation
-------                              ------------
declare operators 0, 1: -> Nat       dec op 0, 1: -> Nat
display rewrite-rules                dis r-r

When an argument to a command can contain reserved words (such as formulas) and names of facts, abbreviations used for reserved words must not conflict with any name-prefix established by the set command. For example, disp form is a legal abbreviation for the command display formulas unless the user has previously entered the command set name form, in which case LP interprets disp form as a request to display all facts whose name begins with the prefix form rather than to display all facts that are formulas.