LP, the Larch Prover -- The write-mode setting
The write-mode setting controls the manner in which the write
command outputs identifiers and terms.
<set-write-mode-command> ::= set write-mode <qualification-mode>
set write-mode qualified
The write-mode setting controls the output of identifiers and terms by
the write command in the current proof context.
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.
qualified print qualifications for all subterms, identifiers
unqualified print no qualifications
unambiguous print enough qualifications to enable reparsing