coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
- To: Coq Club <coq-club AT inria.fr>
- Cc: jonikelee AT gmail.com
- Subject: Re: [Coq-Club] Erasable Red/Black Trees in Coq
- Date: Wed, 23 Apr 2014 09:18:14 +0200
On 23 April 2014 11:17, AUGER Cédric <sedrikov AT gmail.com> wrote:
If you can decide of some property, then you have a form of irrelevance.
Any function to the 'bool' type can be converted in a function to
'Prop' by composition with 'conv (fun x => if x then True else False) :
bool -> Prop'. And for any boolean 'b', a term of type 'conv b' is
"irrelevant" (there is only a single habitant to that type).
That is mainly the main reason why we have UIP on decidable equalities.
This is, however, not sufficient for the trick I mentioned which needs conversion-level irrelevance. Which, indeed, isn't implemented in the current Coq. So, unfortunately, there is no conversion-level associativity yet in Coq. But we can hope the future makes it available.
- [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/21/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Gabriel Scherer, 04/22/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Cedric Auger, 04/22/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/22/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/22/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/22/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/22/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, AUGER Cédric, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/24/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/24/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/24/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/24/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/24/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/24/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/26/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, AUGER Cédric, 04/26/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, AUGER Cédric, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/23/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Arnaud Spiwack, 04/22/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Jonathan, 04/22/2014
- Re: [Coq-Club] Erasable Red/Black Trees in Coq, Gabriel Scherer, 04/22/2014
Archive powered by MHonArc 2.6.18.