coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
- To: Vladimir Voevodsky <vladimir AT ias.edu>
- Cc: Jeremy Avigad <avigad AT cmu.edu>, Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] coercing equality proofs
- Date: Wed, 29 Jan 2014 07:00:12 +0100
There is another way to define bracket in Coq. Something like that:Inductive bracket ( A : Type ) : Prop := wit : A -> bracket A .
Precisely that, indeed. It is, of course, equivalent to the impredicative definition Jeremy used.
- [Coq-Club] coercing equality proofs, Leonardo de Moura, 01/28/2014
- Re: [Coq-Club] coercing equality proofs, Jason Gross, 01/28/2014
- Re: [Coq-Club] coercing equality proofs, Vladimir Voevodsky, 01/28/2014
- Re: [Coq-Club] coercing equality proofs, Jeremy Avigad, 01/28/2014
- Re: [Coq-Club] coercing equality proofs, Jason Gross, 01/28/2014
- Re: [Coq-Club] coercing equality proofs, Cody Roux, 01/28/2014
- Re: [Coq-Club] coercing equality proofs, Jason Gross, 01/28/2014
- Re: [Coq-Club] coercing equality proofs, Cody Roux, 01/28/2014
- Re: [Coq-Club] coercing equality proofs, Jason Gross, 01/28/2014
- Re: [Coq-Club] coercing equality proofs, Cody Roux, 01/28/2014
- Re: [Coq-Club] coercing equality proofs, Vladimir Voevodsky, 01/28/2014
- Re: [Coq-Club] coercing equality proofs, Bas Spitters, 01/29/2014
- Re: [Coq-Club] coercing equality proofs, Arnaud Spiwack, 01/29/2014
- Re: [Coq-Club] coercing equality proofs, Jason Gross, 01/28/2014
- Re: [Coq-Club] coercing equality proofs, Jason Gross, 01/28/2014
- Re: [Coq-Club] coercing equality proofs, Jeremy Avigad, 01/28/2014
- Re: [Coq-Club] coercing equality proofs, Vladimir Voevodsky, 01/28/2014
- Re: [Coq-Club] coercing equality proofs, Jason Gross, 01/28/2014
Archive powered by MHonArc 2.6.18.