[Agda] Do-notation with mix fix binders?

[Jean-Philippe Bernardy]

On Thu, Oct 27, 2011 at 11:28 AM, Dominique Devriese
<dominique.devriese at gmail.com> wrote:

> but the result isn't extremely nice, requiring you to write do on
> every line and the "then"'s everywhere.

I think that it is known how to change the parser to drop the "do" part
(Nils Anders & Ulf have a paper about it) but it is not currently implemented
in Agda.

Cheers,
JP.