<div dir="ltr">Hi, it's useful when you want to often use it with other operators, e.g.:<br><br>data Bla : Set where<br>  bla : Bla<br><br>_B+_ : Bla -> Bla -> Bla<br>_B+_ _ _ = bla<br><br>infixr 30 _B+_<br><br>data Thing : Set where<br>  op_ : Bla -> Thing<br><br>b : Thing<br>b = op bla B+ bla<br><br>This doesn't work if op_ is not an operator.<br><br>======<br>Georgi</div>