coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about a lemma concerning vectors

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/09/2014
- Re: [Coq-Club] Question about a lemma concerning vectors, Frédéric Blanqui, 11/12/2014