LP, the Larch Prover -- The write command
The write command creates a file containing commands that can be executed
to recreate LP's current logical system.
<write-command> ::= write <file> [ <names> ]
Examples
write axioms
write intSet int, set
Usage
The write command creates a file named <file>.lp (unless <file>
contains a period, in which case LP does not supply the suffix .lp) in LP's
current working directory. This file can be executed later with the
execute command to recreate the named set of facts (or the whole
system, if no names are specified). In particular, LP writes
declarations for all identifiers in the named set of facts
followed by commands to register ordering constraints for the facts and
to assert the facts.
Unlike the freeze command, the write command does
not save information about the state of uncompleted proofs. But unlike thawing
a frozen file, which replaces all of LP's logical system, executing a written
file adds information to the current system. Hence it can be used to combine
axiomatizations.
Rewrite rules written by the write command are asserted as formulas.
The numeric extensions in the names assigned to facts
may change when the .lp file is executed; hence facts that are
ancestor-immune may behave differently when the
system is recreated.
See also