Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] coercing equality proofs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] coercing equality proofs


Chronological Thread 
  • 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.



Archive powered by MHonArc 2.6.18.

Top of Page