LP, the Larch Prover -- Keywords


The keywords by, else, if, in, then, when, and yield cannot be used as identifiers for sorts, variables, or operators.

The keywords to and with cannot be used as names for facts, or as components of a name pattern.

LP reserves other words (ac, commutative, depth, on, sort, using and well) in certain contexts within facts and conjectures, but does not prohibit their use as identifiers.