[Agda] Type and termination checking around with clauses

[Peter Berry]

2008/4/30 Anton Setzer <A.G.Setzer at swansea.ac.uk>:
>
>  It sounds to me odd that this solution is accepted, but the direct solution
>  is not accepted.
>  It shouldn't make any difference whether I make a recursive call
>  to merge using a with clause or whether I use it directly.

Bugs are like that :)

[Anton: sorry, forgot to reply to all at first]

-- 
Peter Berry <pwberry at gmail.com>
Please avoid sending me Word or PowerPoint attachments.
See http://www.gnu.org/philosophy/no-word-attachments.html