Stream: Ltac2

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

Louise Dubois de Prisque (Sep 19 2023 at 07:23):

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

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).

Louise Dubois de Prisque (Sep 19 2023 at 07:32):

Great ! Thank you again !!

Notification Bot (Sep 19 2023 at 07:33):

Louise Dubois de Prisque has marked this topic as resolved.

Last updated: Oct 12 2024 at 12:01 UTC