[Agda] {} for nested `with' syntax

Nils Anders Danielsson nad at cse.gu.se
Tue Feb 21 10:32:53 CET 2017


On 2017-02-15 12:45, Sergei Meshveliani wrote:
> A nested `with' construct often requires repeating a large pattern, so
> that a program becomes difficult to read.

For some related discussion, see Issue 510:

   https://github.com/agda/agda/issues/510

-- 
/NAD


More information about the Agda mailing list