20070723-1

In the attached file

Attach:K.agda

the function prop1 doesn't termination check if the last line is replaced with the commented out one. Should it do so by a lexicographic recursion on the term and its type? I tried adding the type explicitly but this didn't help.

I think your problem is the following:

foo : {A : Set} -> List A -> List A
foo []             = []
foo (x :: [])      = []
foo (x :: y :: xs) = foo (y :: xs)

The termination checker can't see that y :: xs is smaller than x :: y :: xs. Also to allow you to omit the type (over which the recursion is done), bug 20070604-1 would have to be fixed.

- Ulf

Fixed. y :: xs is now recognisably smaller than x :: y :: xs.