Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Re: Ltac automation.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: Ltac automation.


chronological Thread 
  • From: "gallais @ EnsL.org" <guillaume.allais AT ens-lyon.org>
  • To: Tom Prince <tom.prince AT ualberta.net>
  • Cc: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Re: Ltac automation.
  • Date: Fri, 11 Feb 2011 12:27:09 +0100
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type :content-transfer-encoding; b=NRX6ov9EtnW0Kfv56kmbg9laPZoDU+GgW9Xvnm363geBp2RDAjlnMkImkFp9LfgmUn bXGapZCCJUN7qe9GnGm6r76X3QgGdp21M2+/Xr7/AEAwn6A9oWJTR0LkCA2qTjfgS3u6 mTWW/yQRlH6zERUcd61/8D7VTWsHocOQWlvUU=
It is not completely true. See the following example that works under 8.3:

(* use n Thm Hyp consumes the hypothesis Hyp to produce a thm based
on Thm *)
Ltac use n Thm Hyp := let H := fresh "H" in match constr:n with
  | 0 => assert (H := Thm Hyp)
  | 1 => assert (H := Thm _ Hyp)
  | 2 => assert (H := Thm _ _ Hyp)
end ; clear Hyp.

Cheers,

--
guillaume



On 11 February 2011 03:47, Tom Prince 
<tom.prince AT ualberta.net>
 wrote:
> it fails. It seems to be that it is impossible to do anything with
> numbers destined to be used as tactic arguments, other than pass them
> around.
>
>  Tom
>


Archive powered by MhonArc 2.6.16.

Top of Page