coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Induction over ascii

From: Marcus Ramos <marcus.ramos AT univasf.edu.br>
To: AUGER Cédric <sedrikov AT gmail.com>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Induction over ascii
Date: Thu, 24 Oct 2013 17:27:33 -0200

Hi Auger,

Thank you for the reply and the hint, now I understand it. Also for the suggestion of flipping the bit, but my main concern is indeed the proof, not the function itself. 

On the other hand, do you know where I can get an explanation of the semantics of "intros [[][][][][][][][]]"? Neither the Reference Manual nor Coq'Art helped me in that. Is there an alternative way of splitting all 256 goals?

Best Regards,
Marcus.

[Coq-Club] Induction over ascii, Marcus Ramos, 10/24/2013
- Re: [Coq-Club] Induction over ascii, t x, 10/24/2013
  - Re: [Coq-Club] Induction over ascii, Marcus Ramos, 10/24/2013
- Re: [Coq-Club] Induction over ascii, AUGER Cédric, 10/24/2013
  - Re: [Coq-Club] Induction over ascii, Marcus Ramos, 10/24/2013
    - Re: [Coq-Club] Induction over ascii, AUGER Cédric, 10/24/2013
      - Re: [Coq-Club] Induction over ascii, Marcus Ramos, 10/24/2013
        
        Re: [Coq-Club] Induction over ascii, AUGER Cédric, 10/24/2013
- <Possible follow-up(s)>
- Re: [Coq-Club] Induction over ascii, txrev319, 10/24/2013
  - Re: [Coq-Club] Induction over ascii, Marcus Ramos, 10/24/2013
    - Re: [Coq-Club] Induction over ascii, Chris Dams, 10/24/2013