coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Posting my first bigger stuff (for experience/training)

From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Posting my first bigger stuff (for experience/training)
Date: Tue, 5 Nov 2013 23:24:02 +0200

Thanks to all for great hints. :) (And apologies for late answer.)

So I removed nz_type and made fin as this Definition fin l := {n | n <= l}, ignoring the idea of empty vectors.
Also I proved that Theorem fin_t1 {l} (n m: fin l): n = m <-> projT1 n = projT1 m. It made everything much easier (thanks to Cedric Auger).

[Coq-Club] Posting my first bigger stuff (for experience/training), Ilmārs Cīrulis, 11/01/2013
- Re: [Coq-Club] Posting my first bigger stuff (for experience/training), Ilmārs Cīrulis, 11/01/2013
  - Re: [Coq-Club] Posting my first bigger stuff (for experience/training), Adam Chlipala, 11/01/2013
- Re: [Coq-Club] Posting my first bigger stuff (for experience/training), AUGER Cédric, 11/02/2013
- Message not available
  - Re: [Coq-Club] Posting my first bigger stuff (for experience/training), Ilmārs Cīrulis, 11/05/2013
    - Re: [Coq-Club] Posting my first bigger stuff (for experience/training), Ilmārs Cīrulis, 11/06/2013
      - Re: [Coq-Club] Posting my first bigger stuff (for experience/training), AUGER Cédric, 11/07/2013
        
        Re: [Coq-Club] Posting my first bigger stuff (for experience/training), Ilmārs Cīrulis, 11/07/2013
        
        Re: [Coq-Club] Posting my first bigger stuff (for experience/training), Cedric Auger, 11/07/2013
        
        Re: [Coq-Club] Posting my first bigger stuff (for experience/training), Ilmārs Cīrulis, 11/13/2013
        [Coq-Club] autorewrite for hypothesis?, Soegtrop, Michael, 11/13/2013
        Re: [Coq-Club] autorewrite for hypothesis?, Jason Gross, 11/13/2013
        RE: [Coq-Club] autorewrite for hypothesis?, Soegtrop, Michael, 11/13/2013
        Re: [Coq-Club] autorewrite for hypothesis?, Eric Mullen, 11/13/2013
        RE: [Coq-Club] autorewrite for hypothesis?, Soegtrop, Michael, 11/14/2013