coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Dependently-typed binary operators

From: Frederic Blanqui <Frederic.Blanqui AT loria.fr>
To: Adam Chlipala <adamc AT cs.berkeley.edu>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Dependently-typed binary operators
Date: Tue, 13 Sep 2005 09:49:59 +0200 (CEST)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

in http://color.loria.fr/, you can find a library on vectors. in the file Util/Vector/VecUtil.v, there are useful lemmas and tactics about vectors.
in your case, the tactic VSntac may be useful. best regards.

[Coq-Club] Dependently-typed binary operators, Adam Chlipala
- Re: [Coq-Club] Dependently-typed binary operators, roconnor
  - Re: [Coq-Club] Dependently-typed binary operators, roconnor
    - Re: [Coq-Club] Dependently-typed binary operators, Pierre Casteran
    - Re: [Coq-Club] Dependently-typed binary operators, Conor McBride
      - Re: [Coq-Club] Dependently-typed binary operators, roconnor
        
        Re: [Coq-Club] Dependently-typed binary operators, Conor McBride
- Re: [Coq-Club] Dependently-typed binary operators, Frederic Blanqui