Operator Syntax

The syntax keyword followed by operator declares a function to be an operators. These operators often have distinct associativity and precedence from regular functions. The operator declaration associates a term with one fixity which define its arity and potentially its precedence and associativity. The operator syntax declaration has to precede the term declaration.

syntax operator <name> <fixity>;

Here <fixity> is a previously declared fixity. Note that there are already many common fixities included in the standard library. See common fixities for more information.

For instance, we can define the × operator as a binary operator:

syntax fixity product := binary;

syntax operator × product;

type × (a : Type) (b : Type) := , : a → b → a × b;