[Agda] a termination problem

[Ramana Kumar]

Wow, I would never have found that myself, thanks :)
Is there any information or papers on sized types I could look at? (Or
do you want to give a brief description here?)

I have further similar termination problems later on in my
development... I'll see if the same trick works! If not, maybe there
is work on improving sized types support I could do?

On Wed, Nov 30, 2011 at 12:18 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> Hello Ramana,
>
> On 29.11.11 11:38 PM, Ramana Kumar wrote:
>>
>> Apart from the feeling that "there must be a better way", I also have
>> a real problem to do with termination.
>> In particular, I define a recursive function that passes itself to
>> Relation.Binary.List.StrictLex.transitive.
>> How can I convince Agda that transitive will only apply it to smaller
>> arguments, or how can I avoid having to try?
>
> This is the typical situation where you would use sized types for
> termination checking.  Unfortunately, the support for sized types is
> rudimentary in Agda at the moment.
>
> However, your example works!  I attach a version of your agda code with a
> sized definition of data type _<_.  [I removed Name since it was not
> available to me, but this is inessential.]
>
> Cheers,
> Andreas
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
>