The Coq mailing list

[Valentin Robert <valentin.robert.42 AT gmail.com>]

Ah, I thought I had tried it earlier, but indeed, it was as simple as this.

Thanks Pierre.

- Valentin

On Fri, Mar 31, 2017 at 3:41 PM Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

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