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