[Agda] Coinductive indices

[Robert J. Simmons]

I'm not quite sure I understand the intuition, but as far as
pattern-matching goes, it works beautifully. Thanks!

On Tue, Mar 15, 2011 at 4:40 PM, Dan Doel <dan.doel at gmail.com> wrote:
> On Tuesday 15 March 2011 4:14:34 PM Robert J. Simmons wrote:
>> data SmallStream' (n : Nat) : Conat → Set where
>>    nil : SmallStream' n zero
>>    cons : ∀{m size}
>>       (N : m ≤ n)
>>       (S : ∞ (SmallStream' n size))
>>       → SmallStream' n (suc (♯ size))
>
> Your definition here is not recommended. Instead, I'd write:
>
>  data SmallStream' (n : Nat) : Conat -> Set where
>    nil : SmallStream' n zero
>    cons : forall {m size}
>       (N : m ≤ n)
>       (S : ∞ (SmallStream' n (♭ size)))
>       -> SmallStream' n (suc size)
>
> The rule being: quantify over an ∞ I, i, make the coinductive reference
> indexed by ♭ i, and make the result type indexed by con i. I being the index
> type of course, and con a constructor.
>
> With this definition, I think you should find it's straight forward to
> implement mark.
>
> -- Dan
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>



-- 
Robert J. Simmons
simrob.com
gps.simrob.com
rjsimmon at cs.cmu.edu
robsimmons at gmail.com
Cell: 404-273-6890