[Agda] Tentative guidelines for working with coinductive types

[Dan Doel]

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".

Well, I don't know how current your Agda install is, or if that'd make a 
difference. I just rebuilt now (apparently I didn't have a version that 
allowed mutual recursion and corecursion), and precisely this works fine for 
me.

That may or may not be helpful, though. :)

-- Dan