coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A question about pattern matching

From: Pierre Casteran <pierre.casteran AT labri.fr>
To: geng chen <chengeng4001 AT gmail.com>
Cc: Chantal Keller <chantal.keller AT wanadoo.fr>, coq-club AT inria.fr
Subject: Re: [Coq-Club] A question about pattern matching
Date: Wed, 03 Feb 2010 09:23:35 +0100

Le 03/02/2010 08:40, geng chen a �crit :

This case is when 'lookup w st = 0'. So why Coq do not put 'lookup w st = 0'
in hypotheses? If I want the 'lookup w st = 0' in the hypotheses, what tactics should I use?

Hello,

Did you try "case_eq (lookup w st)" ?
Pierre

Re: [Coq-Club] A question about pattern matching, geng chen
- Re: [Coq-Club] A question about pattern matching, Pierre Casteran