[Agda] Do-notation with mix fix binders?

Nils Anders Danielsson nad at chalmers.se
Thu Nov 3 18:19:12 CET 2011


On 2011-10-27 11:57, Jean-Philippe Bernardy wrote:
> 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.

I'm not sure exactly what you are referring to here. Can you explain?

-- 
/NAD


More information about the Agda mailing list