Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Issues mixing Ltac, anonymous tactics, eta-expansion

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Issues mixing Ltac, anonymous tactics, eta-expansion


Chronological Thread 
  • From: Pierre Courtieu <pierre.courtieu AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Issues mixing Ltac, anonymous tactics, eta-expansion
  • Date: Sat, 1 Apr 2017 00:40:53 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f46.google.com
  • Ironport-phdr: 9a23:fwcp1x01AiIKikwxsmDT+DRfVm0co7zxezQtwd8Zse0RKfad9pjvdHbS+e9qxAeQG96Kt7Qc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q89pDXbAhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7Vq4/Vyi84Kh3SR/okCYHOCA/8GHLkcx7kaZXrAu8qxBj34LYZYeYP+d8cKzAZ9MXXWhOXshRWSJPAY2ycpUBAPYaMOZEs4XwvUcCoQeiCQSuAu7k1z9GhmXx3a0/y+kvCwDG0xI6H9IUrnvfscv4NKAPUeCv0KnIzCvMb+5L0jr68IjIcw4uoeuWXb1ua8be1U4vFx7fjlWMqIzqIS6V2/8Cs2ie9eVgVOavh3Q7pAF2pzii38EhgZTKiIIN0l3J9yp0zJwoKdGmSEN3e92pHIVKuyyVNoZ7RN4pTXtytyYg0LIGvIa2fCgUx5QjwB7Sc/mHfJKJ4hLnTeqQLzJ4iG58dLKxiBu/8FKsyuL7Vsmz31ZKqjRKnsPQuXAK0hzf8smHSv1j8Ue9wTuC1Q/e5vtZLUwqlafXMZ0szqAqmpccsEnPBir2l1/3jK+SeEUk4O+o6+H/b7X+p5+TKZV0ihvgPag0hsO/Bvk4MhISX2ia5+u8yabu/UL8QLpQj/02lrPVv4zdJcQevqK5GRNa0p4/6xajCDeryMgXnX4eLF5cZB2Hi5XpNErVLfDjDfa/hkysny1xy/DHOL3hGJTNIWLZnLfvZ7Yuo3JbnSE01Jh0449eQuUKJ+u2UUvsvvTZCAU4Okq62bC0Js9609YmWG+VGKLRG6TPq0OJ6/9nd/GNaZUPtXD2LOU/+//jkFc2nFYcee+i2p5BOyPwJehvP0jMOSmkudwGC2pf+1NmFOE=

Did you try to replace your (fun x => ...) by ltac:(fun x => ...)?
Because fun is also the syntax of lambda abstraction in terms.
Not in front of my laptop to check.
Best,
P

2017-04-01 0:18 GMT+02:00 Valentin Robert
<valentin.robert.42 AT gmail.com>:
> Hello,
>
> I was essentially trying to write some tactic combinator that would accept a
> one-argument tactic as input, and call this tactic with some hypothesis. My
> problem is that I have managed to make it work with pre-defined tactics, but
> not with on-the-fly anonymous tactics. See:
>
> Ltac idtac' := idtac.
>
> Ltac idtac'' x := idtac x.
>
> Ltac silly tactic arg := tactic arg.
>
> Goal forall (T : Type), False.
> intros.
>
> (* 0: Illegal tactic application *)
> Fail silly idtac T.
>
> (* 1: Illegal tactic application *)
> Fail silly idtac' T.
>
> (* 2: OK *)
> silly idtac'' T.
>
> (* 3: The reference idtac was not found in the current environment. *)
> Fail silly (fun x => idtac x) T.
>
> (* 4: x not found *)
> Fail silly (fun x => ltac:(idtac x)) T.
>
> (* 5: The reference idtac' was not found in the current environment. *)
> Fail silly (fun x => idtac' x) T.
>
> (* 6: Illegal tactic application *)
> Fail silly (fun x => ltac:(idtac' x)) T.
>
> (* 7: The reference idtac'' was not found in the current environment. *)
> Fail silly (fun x => idtac'' x) T.
>
> (* 8: Cannot infer the type of x in environment:
> T : Type *)
> Fail silly (fun x => ltac:(idtac'' x)) T.
>
> (* 9: Cannot infer an internal placeholder of type "Type" in environment:
> T : Type
> x : Type *)
> Fail silly (fun (x : Type) => ltac:(idtac'' x)) T.
>
> I think by the end of this (attempts 8 and 9), I'm actually confused as to
> what I am manipulating, and what the internal placeholder is.
>
> Is there a way to make such a combinator so that I can call:
>
> silly (fun x => ltac:(someTactic x)).
>
> Or is there some fundamental issue with manipulating anonymous tactics?
>
> Best regards,
> - Valentin



Archive powered by MHonArc 2.6.18.

Top of Page