Skip to content

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;