[Agda] Type and termination checking around with clauses

[Nils Anders Danielsson]

On Wed, Apr 30, 2008 at 2:37 PM, Anton Setzer <A.G.Setzer at swansea.ac.uk> wrote:
>
>  So mergeauxl x xs ys   is essentially merge (x :: xs) ys
>        mergeauxr xs y ys  is essentially merge  xs         (y :: ys)
>        mergeauxlr x xs y ys is essentially merge (x :: xs) (y :: ys)

I sometimes use the same trick (i.e. defining a function f'
corresponding to the application of f to certain constructors) to
coerce the termination checker into accepting my code. It is a bit
ugly, though, since it often involves code duplication.

-- 
/NAD