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.


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


set auto-reg off


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.