Operator Syntax

The syntax keyword, paired with operator, caters for functions serving as operators. These operators often have distinct associativity and precedence from regular functions. The pairing associates a term with one fixity, defining its arity and potentially its precedence and associativity. This syntax declaration has to precede the term declaration.

syntax operator <name> <fixity>;

Where <fixity> is a previously declared fixity. Note that there are already many commons of these declarations included with the standard library. See common fixities for more information.

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

syntax fixity product := binary;

syntax operator × product;

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