The Coq mailing list

[Takashi MIYAMOTO <tmiya AT bu.iij4u.or.jp>]

Dear Pierre,

Thank you for your advice.

On 2012/01/07, at 20:29, Pierre Boutillier wrote:

> Le 7 janv. 12 à 12:14, Takashi MIYAMOTO a écrit :
> 
> You use the dark magie of the return clause (my coq does not find ln 
> definition so this is not tested and there must be typo):

In my first code, I forgot to add "Require Import List". The predicate "In" 
is in the
List library.
I tried the removing the return clause, but the situation was the same.

> (the return clause should be in fact infered)

===================================
Takashi Miyamoto
http://www.imasy.or.jp/~miyamoto/
http://tmiya.blogspot.com/