[Agda] Tentative guidelines for working with coinductive types

[Noam Zeilberger]

On Thu, Jan 15, 2009 at 01:41:48AM +0000, Nils Anders Danielsson wrote:
> On 2009-01-15 01:21, Dan Doel wrote:
> >On Wednesday 14 January 2009 4:51:09 pm Noam Zeilberger wrote:
> >
> >>  infeq : inf ≈ inf
> >>  infeq = seq infeq'
> >>    where infeq' ~ ♯ infeq
> >>
> >>but this doesn't typecheck, because "(ss .T._.inf') != (♭ (♯ inf))
> >>of type CoNat".
> >
> >precisely this works fine for me.
> 
> Yes, this works

well that's bizarre :)  I also just darcs pull'd/recompiled yesterday.
Maybe something to do with the libraries/compiler?  I'm using ghc 6.8.3.

In my version of Agda, you can prove "inf ≈ inf" by proving and then
applying reflexivity, but you can't prove it directly.

Noam