# Mixfix Operators¶

A type name, function name, or constructor name can comprise one or more name parts if we separate them with underscore characters `_`, and the resulting name can be used as an operator. From left to right, each argument goes in the place of each underscore `_`.

For instance, we can join with underscores the name parts `if`, `then`, and `else` into a single name `if_then_else_`. The application of the function name `if_then_else_` to some arguments named `x`, `y`, and `z` can still be written as:

• a standard application by using the full name `if_then_else_ x y z`
• an operator application by placing the arguments between the name parts `if x then y else z`, leaving a space between arguments and part names
• other sections of the full name, for instance leaving one or two underscores:
• `(if_then y else z) x`
• `(if x then_else z) y`
• `if x then y else_ z`
• `if x then_else_ y z`
• `if_then y else_ x z`
• `(if_then_else z) x y`

Examples of type names, function names, and constructor names as mixfix operators:

```-- Example type name _⇒_
_⇒_   : Bool → Bool → Bool
true  ⇒ b = b
false ⇒ _ = true

-- Example function name _and_
_and_ : Bool → Bool → Bool
true and x = x
false and _ = false

-- Example function name if_then_else_
if_then_else_ : {A : Set} → Bool → A → A → A
if true then x else y = x
if false then x else y = y

-- Example constructor name _∷_
data List (A : Set) : Set where
nil  : List A
_∷_ : A → List A → List A
```

## Precedence¶

Consider the expression `true and false ⇒ false`. Depending on which of `_and_` and `_⇒_` has more precedence, it can either be read as `(false and true) ⇒ false = true`, or as `false and (true ⇒ false) = true`.

Each operator is associated to a precedence, which is a floating point number (can be negative and fractional!). The default precedence for an operator is 20.

Note

Please note that `->` is directly handled in the parser. As a result, the precedence of `->` is lower than any precedence you may declare with `infixl` and `infixr`.

If we give `_and_` more precedence than `_⇒_`, then we will get the first result:

```infix 30 _and_
-- infix 20 _⇒_ (default)

p-and : {x y z : Bool} →  x and y ⇒ z  ≡  (x and y) ⇒ z
p-and = refl

e-and : false and true ⇒ false  ≡  true
e-and = refl
```

But, if we declare a new operator `_and’_` and give it less precedence than `_⇒_`, then we will get the second result:

```_and’_ : Bool → Bool → Bool
_and’_ = _and_
infix 15 _and’_
-- infix 20 _⇒_ (default)

p-⇒ : {x y z : Bool} →  x and’ y ⇒ z  ≡  x and’ (y ⇒ z)
p-⇒ = refl

e-⇒ : false and’ true ⇒ false  ≡  false
e-⇒ = refl
```

## Associativity¶

Consider the expression `true ⇒ false ⇒ false`. Depending on whether `_⇒_` is associates to the left or to the right, it can be read as `(false ⇒ true) ⇒ false = false`, or `false ⇒ (true ⇒ false) = true`, respectively.

If we declare an operator `_⇒_` as `infixr`, it will associate to the right:

```infixr 20 _⇒_

p-right : {x y z : Bool} →  x ⇒ y ⇒ z  ≡  x ⇒ (y ⇒ z)
p-right = refl

e-right : false ⇒ true ⇒ false  ≡  true
e-right = refl
```

If we declare an operator `_⇒’_` as `infixl`, it will associate to the left:

```infixl 20 _⇒’_

_⇒’_ : Bool → Bool → Bool
_⇒’_ = _⇒_

p-left : {x y z : Bool} →  x ⇒’ y ⇒’ z  ≡  (x ⇒’ y) ⇒’ z
p-left = refl

e-left : false ⇒’ true ⇒’ false  ≡  false
e-left = refl
```

## Ambiguity and Scope¶

If you have not yet declared the fixity of an operator, Agda will complain if you try to use ambiguously:

```e-ambiguous : Bool
e-ambiguous = true ⇒ true ⇒ true
```
```Could not parse the application true ⇒ true ⇒ true
Operators used in the grammar:
⇒ (infix operator, level 20)
```

Fixity declarations may appear anywhere in a module that other declarations may appear. They then apply to the entire scope in which they appear (i.e. before and after, but not outside).