The commands `defineconstant`, `defineinfix`, `
definetypedinfix`, and `defineopaque` can be used to define
(and automatically declare) constants or operators.

The predeclared operators `@` (function application) and `,`
(ordered pair) have a special role in the definition facility.

A definition introduces an equation whose left side must have a special form.

We first define the class of *argument lists*. A free variable
or iterated constant function of a free variable (built using
brackets) is an argument list. Any pair (built using the `,`
infix) of argument lists is an argument list. All argument lists are
constructed in this way.

If a constant is being defined, the constant itself is a possible left
side for its defining equation. If any term is an admissable left
side, the term built by applying that term to an argument list (using
the `@` infix) is an admissable left side. All admissable left
sides for constant definitions are constructed in this way.

If an operator is being defined, a unary or binary term whose left and
right subterms (the left may, of course, not be present; a default
left argument of `defaultprefix` is automatically declared in this
case) are argument lists is an admissable left side. The result of
applying an admissable left side to an argument list is an admissable
left side. All admissable left sides for operator definitions are
constructed in this way.

Notice that ``curried'' higher order functions can be implicitly defined!

The further conditions on a definition are that the constant or
operator being defined be undeclared, but that all other constants
appearing in the defining equation be declared, that every free
variable occurring on the right side also occur on the left side (no
operator variables may appear in a definition), and that the defining
equation considered as a term (`=` is predeclared and has left and
right types of 0) be stratified.

Implicit function definitions using this procedure are guaranteed to
avoid paradox (they are valid in the context of New Foundations with
urelements). The ability to apply the constant function operator to
variables allows more control over the relative typing of arguments;
attention to relative type is also important when currying is used (a
curried function is *not* equivalent to a similar-looking
function with an argument list built using pairing; relative types are
quite different!).

The `defineitconstant`, `defineitinfix` and `
defineittypedinfix` commands allow one to use the selected subterm
of the right side of the current equation as the right side of a
definition.

Fri Sep 5 16:28:58 MDT 1997