[Agda] Problem with the termination checker

David Leduc david.leduc6 at googlemail.com
Fri Sep 24 17:06:32 CEST 2010


Thank you for your help.

> This is rather a problem with your definition.  (See below.)

I now understand the problem but I cannot find a solution. Any suggestion?
It should be possible to lift a term of type T l.

> Also I do not know what is the purpose of T.

Just for the purpose of example.


More information about the Agda mailing list