[Agda] when to set underscore suffix?

[mechvel at scico.botik.ru]

On 2020-11-23 20:47, Georgi Lyubenov wrote:
> Hi, it's useful when you want to often use it with other operators,
> e.g.:
> 
> data Bla : Set where
>   bla : Bla
> 
> _B+_ : Bla -> Bla -> Bla
> _B+_ _ _ = bla
> 
> infixr 30 _B+_
> 
> data Thing : Set where
>   op_ : Bla -> Thing
> 
> b : Thing
> b = op bla B+ bla
> 
> This doesn't work if op_ is not an operator.
> 


What is an operator?
A function which name has underscore in it?

--
SM