LP, the Larch Prover -- Constants


A constant is a 0-ary operator. An identifier for a constant can be either a <simpleId> (e.g., 0 and c) or a bracketed operator (e.g., {} and []).

The same identifier can be overloaded to name two different constants, that is, two constants with different sorts. A <simpleId> can also be used to name a variable and a constant, provided the variable does not have the same sort as the constant.

When LP formulates hypotheses for use in proving subgoals in a proof, it generally replaces all free variables in the hypotheses by constants. LP creates identifiers for these constants by appending the letter c and, if necessary, further digits to obtain an identifier that is not already in use. Thus LP may replace the variable x by the constants xc, xc1, ...