[Agda] Coinductive families

[Nils Anders Danielsson]

On 2010-10-05 14:14, Andreas Abel wrote:
> Currently records are hybrids, because we have record patterns. If all
> record patterns could be translated away, we could understand records in
> terms of &. But currently we allow record patterns that cannot be
> translated away, such as where record patterns are mixed with data
> constructor patterns.

I'm fairly certain that we can translate away these patterns, but there
is no immediate need to do so, because the translation would be
observationally indistinguishable from what we generate now (modulo any
bugs).

--
/NAD