[Agda] a termination problem

[Ramana Kumar]

I found your MiniAgda paper, and some slides... I had a skim, and
might read in more detail later...
It seems like sizes would have to appear on a lot of stuff in the
standard library for them to really be useful?

I've put my next termination problem here http://hpaste.org/54700.
Can you see a way to use sized types to do this?
I will try myself, but I'm less sure about what's going on.

I look forward to your reply :)

On Wed, Nov 30, 2011 at 10:31 AM, Ramana Kumar <rk436 at cam.ac.uk> wrote:
> 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/
>>
>