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)).