[Agda] Do-notation with mix fix binders?

[Dominique Devriese]

I use something like this in my paper "On the bright side of type
classes: Instance Arguments in Agda". You can define

  syntax bind m (\ x → c) = do x ← m then c

and define

  do_then_ = _>>_

but the result isn't extremely nice, requiring you to write do on
every line and the "then"'s everywhere. You could maybe replace the
"then" with a semicolon or something to get something slightly nicer.
But essentially, you can't get Haskell's layout-sensitive syntax in
this way and as such, a nice solution would require building this in
natively in the parser, similar to Haskell.

Dominique

2011/10/27 Liam O'Connor <liamoc at cse.unsw.edu.au>:
> Hi all,
> Does anyone know of a way to get something like Haskell's do-notation
> (without destructuring assignment) with mix fix syntax binders? It would be
> rather nice if we had such a facility.
> Cheers
> Liam O'Connor
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>