LP, the Larch Prover -- The write-mode setting

The write-mode setting controls the manner in which the write command outputs identifiers and terms.

Syntax

<set-write-mode-command> ::= set write-mode <qualification-mode>

Examples

set write-mode qualified

Usage

The write-mode setting controls the output of identifiers and terms by the write command in the current proof context. 
write-mode         effect
----------         ------
qualified          print qualifications for all subterms, identifiers
unqualified        print no qualifications
unambiguous        print enough qualifications to enable reparsing
The default write-mode is qualified, which guarantees that the output can be reparsed even in the presence of additional overloadings for identifiers. It is often desirable, however, to set the write-mode to unambiguous to shorten and improve the readability of .lp files. If a problem arises in executing a .lp file produced in this fashion (because it is being executed in a context that overloads one of its operators), the problem can be solved by starting a new copy of LP, executing the .lp file, and writing it out again in qualified mode.

See also