coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "John Wiegley" <johnw AT newartisans.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Question about a lemma concerning vectors
- Date: Tue, 11 Nov 2014 00:22:27 -0600
- Organization: New Artisans LLC
>>>>> Emilio Jesús Gallego Arias
>>>>> <gallego AT cri.ensmp.fr>
>>>>> writes:
> tuples in ssr are a pair of a list plus a proof of its size, it may work
> well wrt to extraction (I have never extracted ssr code).
The tuple code seems like it should be in ssreflect proper, next to fintype,
rather than in mathcomp (in 1.5).
John
- Re: [Coq-Club] Question about a lemma concerning vectors, (continued)
- Re: [Coq-Club] Question about a lemma concerning vectors, Cedric Auger, 11/09/2014
- Re: [Coq-Club] Question about a lemma concerning vectors, John Wiegley, 11/09/2014
- Re: [Coq-Club] Question about a lemma concerning vectors, Adam Chlipala, 11/09/2014
- Re: [Coq-Club] Question about a lemma concerning vectors, John Wiegley, 11/10/2014
- Re: [Coq-Club] Question about a lemma concerning vectors, John Wiegley, 11/10/2014
- Re: [Coq-Club] Question about a lemma concerning vectors, Emilio Jesús Gallego Arias, 11/10/2014
- Re: [Coq-Club] Question about a lemma concerning vectors, Cedric Auger, 11/10/2014
- Re: [Coq-Club] Question about a lemma concerning vectors, Cedric Auger, 11/10/2014
- Re: [Coq-Club] Question about a lemma concerning vectors, John Wiegley, 11/10/2014
- Re: [Coq-Club] Question about a lemma concerning vectors, Emilio Jesús Gallego Arias, 11/10/2014
- Re: [Coq-Club] Question about a lemma concerning vectors, John Wiegley, 11/11/2014
- Re: [Coq-Club] Question about a lemma concerning vectors, Emilio Jesús Gallego Arias, 11/10/2014
- Re: [Coq-Club] Question about a lemma concerning vectors, John Wiegley, 11/10/2014
- Re: [Coq-Club] Question about a lemma concerning vectors, John Wiegley, 11/09/2014
- Re: [Coq-Club] Question about a lemma concerning vectors, Emilio Jesús Gallego Arias, 11/09/2014
- Re: [Coq-Club] Question about a lemma concerning vectors, Frédéric Blanqui, 11/12/2014
- Re: [Coq-Club] Question about a lemma concerning vectors, Cedric Auger, 11/09/2014
Archive powered by MHonArc 2.6.18.