LP, the Larch Prover — The set command

The set command controls various aspects of LP's behavior.

Syntax

<set-command>  ::= set [ <setting-name> [ <setting-value> ] ]
<setting-name> ::= activity | automatic-ordering | automatic-registry 
                      | box-checking | completion-mode | directory 
                      | display-mode | hardwired-usage | immunity 
                      | log-file | lp-path | name-prefix | ordering-method
                      | page-mode | prompt | proof-methods 
                      | reduction-strategy | rewriting-limit | script-file
                      | statistics-level | trace-level | write-mode
<setting-value> ::= <string>

Note: The setting-name can be abbreviated.

Examples

set
set proof-methods
set script session

Usage

The set command with no arguments prints the current values of all settings. The set command with a <setting-name> and no <setting-value> displays the current value of the setting and then requests a new value; responding with a carriage return leaves the value of the setting unchanged. The set command with both a <setting-name> and a <setting-value> sets the value of one of the following settings.

Settings marked with (L) are local to the current proof context. If such a setting is changed, for example, during the proof of one case in a proof by cases it reverts to its previous value upon termination of that case in the proof. Settings marked with G are global and remain in effect until changed by the user. All settings have default values, which can be restored by the unset command.

(L) activity ( on | off ): New assertions are active if on (the default).
(L) automatic-ordering ( on | off ): Formulas are oriented automatically into rewrite rules if on (the default).
(L) automatic-registry ( on | off ): The registry is extended automatically during ordering if on (the default).
(G) box-checking ( on | off ): Markings (<>, []) for proof steps are checked in command files if on (the default).
(L) completion-mode ( big | expert | standard ): Controls the action of the complete command (default standard).
(G) directory <file>: Output files are created in this directory (default ".").
(L) display-mode ( qualified | unqualified | unambiguous ): Controls the qualification of identifiers and terms by the display command (default unambiguous).
(L) hardwired-usage <number>: Turns off some hardwired rules.
(L) immunity ( on | off | ancestor ): Controls the immunity of new assertions (default off).
(G) log-file <file>: Creates file <file>.lplog for log of session (default none).
(G) lp-path <string>: Defines search path for help, .lp, .lpfrz files (default . ~/lp).
(L) name-prefix <simpleId>: Defines prefix for names of assertions, conjectures (default user).
(L) ordering-method <ordering>: Defines method for orienting formulas into rewrite rules (default noeq-dsmpos).
(G) page-mode ( on | off ): Output is paged if on (default off).
(G) prompt <string>: Defines LP's command prompt (default `LP! ').
(L) proof-methods <default-proof-method>+[,]: Defines list of default proof methods for conjectured formulas (default normalization).
(L) reduction-strategy ( inside-out | outside-in ): Controls application of rewrite rules to terms (default outside-in).
(L) rewriting-limit <number>: Bounds number of steps in possibly infinite rewrites (default 1000).
(G) script-file <file>: Creates file <file>.lpscr for record of input (default none).
(G) statistics-level <number>: Controls the kinds of statistics kept by LP (default 2).
(G) trace-level <number>: Controls the amount of detailed output produced by LP (default 1).
(L) write-mode ( qualified | unqualified | unambiguous ): Controls the qualification of identifiers and terms by the write command (default qualified).