coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac like destruct .. as ...

From: Jianzhou Zhao <jianzhou AT seas.upenn.edu>
To: vsiles AT lix.polytechnique.fr
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Ltac like destruct .. as ...
Date: Sat, 14 Aug 2010 21:24:57 -0400
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=cSDCYIW6wv867Xeph3Wb7nDwYzjDi/i0xD+F8ux3q7TZJDBFJHdaDBzg4NvYVWkIPT q/EZ5qT4stG8ZDR4JIIOGsnI0/rJfxmFM/+sXGPQu6TdzdSnNphqXIlFH8/c0vcUA+BF 8Tka7LGAcrLz1F9WFQ95cHkJW1sQdV6K9B9us=

On Sat, Aug 14, 2010 at 2:43 AM, Vincent Siles
<vsiles AT lix.polytechnique.fr>
wrote:
>> Hello,
>>
>> I wanted to define a tactical working like
>> � destruct H as J1 J2 ...
>> The list of names of J's is with variant length. �I defined:
>>
>
> Hi,
> I think you are a bit wrong here:
> destruct _ as _ does not take a list of name, but a "intro pattern"[1]
> which is a single object that explains how to name the differents parts
> of the destructed hypothesis.

Yes. The real 'destruct' uses this more complicated pattern than a list.

>
> However, I don't know how to handle them in Ltac, sorry.

Is 'destruct' an internal tactical, or a tactical we can define by
Ltac language?

>
> Cheers,
> Vincent
>
>
>
>
> [1]
> http://coq.inria.fr/refman/Reference-Manual011.html#@tactic82
>

--
Jianzhou

[Coq-Club] Ltac like destruct .. as ..., Jianzhou Zhao
- Re: [Coq-Club] Ltac like destruct .. as ..., Vincent Siles
  - Re: [Coq-Club] Ltac like destruct .. as ..., Jianzhou Zhao