Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


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



Archive powered by MHonArc 2.6.18.

Top of Page