LP, the Larch Prover -- Functional operators


LP allows users to declare symbols for use in ordinary functional notations in terms. A function identifier, or <functionId>, is just a simple identifier, that is, a <simpleId>. It can be used as a constant (e.g., 0) or as an operator that takes a parenthesized list of arguments (e.g., gcd(x, y)).