LP, the Larch Prover — The make command


The make command changes the activity or immunity of a collection of facts or of the current conjecture.

Syntax

<make_command> ::= make <fact-status> ( <names> | conjecture )
<fact-status>  ::= active | passive | immune | nonimmune | ancestor-immune
Note: The <fact-status> can be abbreviated.

Examples

make inactive rewrite-rules
make immune conjecture

Usage

LP automatically uses any rewrite rules made active by the make command to normalize terms appearing in the current conjecture or in nonimmune facts in LP's logical system. It also automatically applies any deduction rules made active by the make command.

LP automatically normalizes any rewrite rules and deduction rules made nonimmune by the make command, and it applies all active deduction rules to these deimmunized rules.

See the activity and immunity settings.