LP, the Larch Prover — The box-checking setting

The box-checking setting governs whether or not LP checks for the presence of annotations marking the beginning and end of proofs steps in files being executed by the execute command.

Syntax

<set-box-checking-command> ::= set box-checking ( on | off )

Examples

set box on

Usage

LP checks <>'s and []'s when it executes commands from a .lp file and box-checking is on. It ignores these annotations when box-checking is off.

See the box and diamond commands for details.