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

[Nils Anders Danielsson]

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.

-- 
/NAD