Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] A not so FSet specific question about destruction

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A not so FSet specific question about destruction


chronological Thread 
  • From: St�phane Lescuyer <stephane.lescuyer AT inria.fr>
  • To: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] A not so FSet specific question about destruction
  • Date: Mon, 19 Oct 2009 16:59:50 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; b=Q1T51SHxa5balLnou2vAhofaseVJFnYEhfTOwaVsRHv9t3u6bXGX1ilxq+TwV8DGE9 kgb3fraYLiNrtYpwkT/SAMLZ5Oz5wV0GPRYnXja3wL+91LsXjGSj0orDiVi44uajgWBJ INyPJF1EtEca5xWtQnFawZ0JZN72nsuT61azg=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On Mon, Oct 19, 2009 at 4:50 PM, Guillaume Melquiond
<guillaume.melquiond AT inria.fr>
 wrote:
> Stephane's solution is correct. I would just like to point that there is a
> better tactic than "destruct" for this kind of inductives:
>
>  case mem_eq. (* No arguments! Coq infers them when using "case". *)
>

Good to know, indeed ! Any particular reason why destruct does not do
something similar ? Or does not accept holes, which would be
sufficient for that matter : destruct (mem_eq _ _) ?

Stéphane

-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06



Archive powered by MhonArc 2.6.16.

Top of Page