[Agda] Coinductive families

[Nils Anders Danielsson]

On 2010-10-05 13:58, Andreas Abel wrote:
>
> On Oct 5, 2010, at 2:52 PM, Thorsten Altenkirch wrote:
>
>> Could we not view record types as data types with one constructor?
>
> Not always, since record patterns are translated away sometimes.

And primitive record patterns break subject reduction in the presence of
η-equality:

   http://code.google.com/p/agda/issues/detail?id=276

--
/NAD