The Coq mailing list

[Shigeo Nishi <shigeonishi AT hotmail.com>]

I'm reading some chapters from Pierce's and started reading CPDT book. I'm currently interested in using Coq for program verification, so I came up with this question.

Thanks a lot.

---

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

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.