LP, the Larch Prover — The completion-mode setting


The completion-mode setting sets the operating mode for the completion procedure.

Syntax

<set-completion-mode-command> ::= set completion-mode <completion-mode>
<completion-mode>             ::= standard | expert | big
Note: The <completion-mode> can be abbreviated.

Examples

set completion-mode expert

Usage

The completion-mode setting affects the order in which completion tasks are executed in the current proof context. It also affects the amount of user interaction during the completion procedure.