coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however .....

From: Adam Chlipala <adamc AT csail.mit.edu>
To: Shigeo Nishi <shigeonishi AT hotmail.com>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however .....
Date: Sat, 07 Sep 2013 20:06:54 -0400

On 09/07/2013 08:01 PM, Shigeo Nishi wrote:

I'm a Coq beginner, but I think I have a question that has to do with this thread since I'm trying to prove that an inductive proposition with the wrong "evidence" is evaluated to False.

[...]

I'm stuck in this goal:

1 subgoals
H0 : isof2 (1 :: nil)
______________________________________(1/1)
False

What source are you using to learn Coq? I expect most will introduce the tools you need here, probably as part of an introduction to inductive predicates.

[Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Satrajit Roy, 09/07/2013
- Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., t x, 09/07/2013
- Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Adam Chlipala, 09/07/2013
  - Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Andrew Hirsch, 09/08/2013
    - RE: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Shigeo Nishi, 09/08/2013
      - Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Adam Chlipala, 09/08/2013
        
        RE: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., Shigeo Nishi, 09/08/2013
        
        Re: [Coq-Club] Not sure if this is the right forum for beginners' questions, however ....., t x, 09/08/2013