[Agda] when to set underscore suffix?

[Georgi Lyubenov]

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.

======
Georgi
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201123/8b42c714/attachment.html>