coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] equality of equality of equality of equality

From: Andrej Bauer <andrej.bauer AT andrej.com>
To: Vladimir Voevodsky <vladimir AT ias.edu>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] equality of equality of equality of equality
Date: Fri, 18 May 2012 10:22:22 +0200

> Definition eqnplus1 ( n:nat ) {X : Type} ( x y : X) : Type.
> Proof. here follow the "destruct n" with eq X x y for n=0 and the obvious
> step for n+1. Defined.

The obvious step elludes me. Also, did you mean "destruct n" or "induction n"?

With kind regards,

Andrej

[Coq-Club] equality of equality of equality of equality, Andrej Bauer, 05/15/2012
- Re: [Coq-Club] equality of equality of equality of equality, Adam Chlipala, 05/15/2012
- Re: [Coq-Club] equality of equality of equality of equality, Daniel Schepler, 05/16/2012
  - Re: [Coq-Club] equality of equality of equality of equality, Favonia, 05/16/2012
    - Re: [Coq-Club] equality of equality of equality of equality, Andrej Bauer, 05/16/2012
      - Re: [Coq-Club] equality of equality of equality of equality, AUGER Cédric, 05/16/2012
        
        Re: [Coq-Club] equality of equality of equality of equality, Andrej Bauer, 05/16/2012
        
        Re: [Coq-Club] equality of equality of equality of equality, AUGER Cédric, 05/16/2012
        
        Re: [Coq-Club] equality of equality of equality of equality, AUGER Cédric, 05/17/2012
- Re: [Coq-Club] equality of equality of equality of equality, Vladimir Voevodsky, 05/17/2012
  - Re: [Coq-Club] equality of equality of equality of equality, Andrej Bauer, 05/18/2012
    - Re: [Coq-Club] equality of equality of equality of equality, Andrej Bauer, 05/18/2012
      - Re: [Coq-Club] equality of equality of equality of equality, Daniel Schepler, 05/19/2012
        
        Re: [Coq-Club] equality of equality of equality of equality, Daniel Schepler, 05/20/2012