
module Syntax.Infix where

open import Sets.Enumerated using (Bool; true; false)

Infix notation

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.)

Infix Notation