[Agda] Coinductive families

[Nicolas Pouillard]

On Tue, 05 Oct 2010 16:29:05 +0100, Nils Anders Danielsson <nad at Cs.Nott.AC.UK> wrote:
> 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).

I was also thinking that one could translate them away, namely using 'with'
on projections.

foo (true  , x) = e1
foo (false , x) = e2

would become

foo p with proj₁ p
... | true   = e1[ x := proj₂ p ]
... | false  = e2[ x := proj₂ p ]

So I would think that one can understand records as being used by there
projections.

Regards,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr