[Agda] Coinductive families

[Nicolas Pouillard]

On Thu, 7 Oct 2010 23:19:01 +0200, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> Ok, this works, but anyway, I think inductive records are doomed.
> 
> Eta-expansion does not terminate for inductive record like List so I  
> guess there will be soon a check to rule them out.

Even those where recursion is broken using a 'data' type like Box?

-- 
Nicolas Pouillard
http://nicolaspouillard.fr