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