LP, the Larch Prover — The automatic-registry setting

The automatic-registry setting controls whether LP asks the user to confirm extensions to the registry when formulas are oriented into rewrite rules.

Syntax

<set-automatic-registry-command> ::= set automatic-registry ( on | off )

Examples

set auto-reg off

Usage

If automatic-registry is on (the default), then LP automatically extends its registry, if necessary, when using a registered ordering to orient formulas into rewrite rules. If it is off, LP prompts the user to select one of a list of possible extensions whenever the registry must be extended. When it is off, LP also gives users the opportunity to divide incompatible equations and to orient formulas manually.