coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: David Leduc <david.leduc6 AT googlemail.com>
- To: Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Equational Reasoning over streams
- Date: Sat, 23 Oct 2010 07:52:22 +0000
- Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; b=INKGcJG6SbMNYyZZDvDxXTElnm/uk9a8aH5yKi3UvqHFaSs0Jr0oqEuBbNoVPiROiA 0KrYqo9N60tGv4Qqk0nJwdmr1wgjd1A43LvxUstplcKKOXs8QF1ibifaFIB6A+KqOjDc NCPky8j+VdTZZ7HWT6Iusy7J845XCS5cqI58I=
> I think you can use Mendler style to nest induction into coinducation if
> you like.
What is Mendler's style?
I cannot find any example in Coq in your paper and your slides :(
- [Coq-Club] recursive Ltac definitions, Aaron Bohannon
- [Coq-Club] Re: recursive Ltac definitions,
Aaron Bohannon
- [Coq-Club] Equational Reasoning over streams,
Herman Geuvers
- Re: [Coq-Club] Equational Reasoning over streams,
Thorsten Altenkirch
- Re: [Coq-Club] Equational Reasoning over streams,
David Leduc
- Re: [Coq-Club] Equational Reasoning over streams,
Herman Geuvers
- Re: [Coq-Club] Equational Reasoning over streams, AUGER Cedric
- Re: [Coq-Club] Equational Reasoning over streams,
Keiko Nakata
- Re: [Coq-Club] Equational Reasoning over streams, David Leduc
- Re: [Coq-Club] Equational Reasoning over streams,
Herman Geuvers
- Re: [Coq-Club] Equational Reasoning over streams,
David Leduc
- Re: [Coq-Club] Equational Reasoning over streams,
Thorsten Altenkirch
- [Coq-Club] Equational Reasoning over streams,
Herman Geuvers
- Re: [Coq-Club] recursive Ltac definitions, Adam Chlipala
- [Coq-Club] Re: recursive Ltac definitions,
Aaron Bohannon
Archive powered by MhonArc 2.6.16.