LP, the Larch Prover — The name-prefix setting

The name-prefix setting specifies the identifier used to construct names for newly asserted facts and conjectures.

Syntax

<set-name-prefix-command> ::= set name-prefix <simpleId>

Examples

set name nat

Usage

The set name-prefix command directs LP to use the <simpleId> as the prefix for any new names generated in the current proof context. After a command such set name nat, LP assigns the names nat.1, nat.2, ... in sequence to facts and conjectures.