module Syntax.Infix where open import Sets.Enumerated using (Bool; true; false)

Consider this definition:

data BinTree' : Set where x : BinTree' _+_ : BinTree' → BinTree' → BinTree'

There one can note that it basically yields the following:

```
BinTree' : Set
x : BinTree'
x + x : BinTree'
(x + x) + x : BinTree'
x + (x + x) : BinTree'
(x + x) + (x + x) : BinTree'
...
```

Underscores in names — like `_+_`

above — are placeholders for operands.

One can also give the precedence with `infix`

, (non-associative), `infixl`

(left-associative) or `infixr`

(right-associative).

For example the single line below:

infixr 3 _+_

yields the following:

```
BinTree' : Set
x : BinTree'
x + x : BinTree'
(x + x) + x : BinTree'
x + x + x : BinTree'
(x + x) + x + x : BinTree'
...
```

(So, now `_+_`

has the right precedence, and it became right-associative.)