
module Syntax.Infix where

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

Infix notation


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

yields

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

Underscores in names like _+_ denote the space for the operands.

One can give the precedence with infix, infixl or infixr:


infixr 3 _+_

yields

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

(so _+_ has right precedence)

Infix Notation