[Agda] eta expansion

[Nils Anders Danielsson]

On 2013-03-09 10:03, Andreas Abel wrote:
> Some comments on your points:
>
> (0) I do not understand.

Me neither.

> (2)--(3) The termination checker has not been justified for
> induction-recursion, at least I never looked at these types formally.

Another issue: size-change termination. Vytiniotis, Coquand and
Wahlstedt's "Stop When You Are Almost-Full - Adventures in Constructive
Termination" gives a constructive explanation of size-change
termination. However, I don't think anyone has showed that one can
compile something like Agda to some kind of core language without
size-change termination in a definitional-equality-preserving way.

-- 
/NAD