coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Pierre Lescanne (at work)" <pierre.lescanne AT ens-lyon.fr>
- To: coq-club AT inria.fr
- Cc: pierre.lescanne AT ens-lyon.fr
- Subject: Re: [Coq-Club] inversion of an inductive
- Date: Sat, 16 Apr 2016 10:00:43 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.lescanne AT ens-lyon.fr; spf=Pass smtp.mailfrom=pierre.lescanne AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
- Ironport-phdr: 9a23:uxjRMxzV3D2kRYTXCy+O+j09IxM/srCxBDY+r6Qd0eMSIJqq85mqBkHD//Il1AaPBtWLra8UwLSM+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuSt6U0pT8ibr60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyZb1eFjUvdW4vt/fmrR3ScQza/noRSH8b1B5FGAPM6hf3dpr3qW7+p+17nieAbuPsSrVhEwyj4r1xRVfMhTwMPjg//SmXg9A4k6VBo1Pr70hnwoPOeozTMPdldarbe94ySGxaG8JAUCoHDJnqPNhHNPYIIesN99q1nFAJtxbrXQQ=
|
Thank you Adam and Jean-François for your answers which are very
useful. Being able to use inversion, together with coinductive
objects and dependent types is very central in what I want to do
and I know now that this is possible and can be done simply. Le 15/04/2016 19:37, Pierre Lescanne
(at work) a écrit :
I have developed in Coq exercises in extensive game theory (for economics). A first development was with coinductive. In this development I was able to perform inversion. -- Best wish --------------------------- Pierre Lescanne (Emeritus Professor) LIP / École normale supérieure de Lyon 46 allée d'Italie 69364 LYON Cedex 07, France tél: +33 6 85 70 94 31 http://perso.ens-lyon.fr/pierre.lescanne/ --------------------------- |
- [Coq-Club] inversion of an inductive, Pierre Lescanne (at work), 04/15/2016
- Re: [Coq-Club] inversion of an inductive, Adam Chlipala, 04/15/2016
- Re: [Coq-Club] inversion of an inductive, Jean-Francois Monin, 04/15/2016
- Re: [Coq-Club] inversion of an inductive, Pierre Lescanne (at work), 04/16/2016
Archive powered by MHonArc 2.6.18.