coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "psperatto AT adinet.com.uy" <psperatto AT adinet.com.uy>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] inductive
- Date: Wed, 29 Aug 2012 16:54:16 -0300 (UYT)
Do you know if there is some paper or book that presents
the definition of the rec, rect, ind (the elimination
and equality rules) from the type former and
construction rules of an inductive set (type, prop)?
Regards
Patricia Peratto
- [Coq-Club] inductive, psperatto AT adinet.com.uy, 08/29/2012
- Re: [Coq-Club] inductive, Adam Chlipala, 08/29/2012
Archive powered by MHonArc 2.6.18.