[Agda] Termination and efficiency of higher order functions over nested datatypes

[Alan Jeffrey]

Ah, that did the trick, although "broken" and "not... happy" don't fill 
me with glee :-)

A.

On 09/28/2011 03:55 AM, Nils Anders Danielsson wrote:
> On 2011-09-28 04:34, Alan Jeffrey wrote:
>> In an ideal world, there'd be some way to persuade the termination
>> checker that map is a non-increasing function. Is such a thing feasible?
>
> You can do this using sized types. However, as far as I know Agda's
> sized types machinery (--sized-types) is currently broken in some way,
> and we have not found a source language design we're really happy with.
>