Stream: Ltac2

Topic: ✔ Use of Ltac1.run, Ltac1.apply and Ltac1.of_ident


view this post on Zulip Louise Dubois de Prisque (Sep 18 2023 at 14:44):

Hello, I am trying to use (in Coq 8.17) the functions Ltac1.run and Ltac1.apply from Ltac2. But I am doing something wrong and I don't understand the problem. Here is a minimal example:

Goal True -> True.
Fail Ltac1.run (Ltac1.of_ident (@intros)).

(* The command has indeed failed with message:
Expression does not evaluate to a tactic. *)

Ltac1.apply (Ltac1.of_ident (@intros)) [] Ltac1.run.

(*The command has indeed failed with message:
 Variable F should be bound to a tactic. *)

In the first example, the error message is strange because intros is indeed a tactic, and not a Ltac1 value. So maybe the problem leads in my use of Ltac1.of_ident ?
In the second example, the error message is difficult to understand, maybe it is linked to a similar problem.

If you have some working examples on how to use these functions, that would be really helpful !

Thank you in advance for your help :)

view this post on Zulip Gaëtan Gilbert (Sep 18 2023 at 15:07):

of_ident produces a ltac1 value which is the given ident
What you want is something which resolves the ident to the ltac1 it is bound to in some environment. I don't think we provide such an API currently.

Basically you're getting the same result as

Tactic Notation "foo" ident(x) := x.

Goal True.
  foo intros.
(* Expression does not evaluate to a tactic. *)

view this post on Zulip Louise Dubois de Prisque (Sep 19 2023 at 07:23):

Thank you @Gaëtan Gilbert ! How can I use run or apply correctly then?

view this post on Zulip Gaëtan Gilbert (Sep 19 2023 at 07:27):

Require Import Ltac2.Ltac2.

Goal True -> True -> True.
Proof.
  Ltac1.run ltac1val:(intros x).
  Ltac1.apply ltac1val:(fun H => intros H) [Ltac1.of_ident ident:(y)] (fun tac => Ltac1.run tac).

view this post on Zulip Louise Dubois de Prisque (Sep 19 2023 at 07:32):

Great ! Thank you again !!

view this post on Zulip Notification Bot (Sep 19 2023 at 07:33):

Louise Dubois de Prisque has marked this topic as resolved.


Last updated: May 18 2024 at 08:40 UTC