Stream: Ltac2

Topic: ✔ Unpacking lists of arguments

Gaëtan Gilbert (Dec 04 2023 at 16:02):

use Std.pattern not the pattern notation

Gaëtan Gilbert (Dec 04 2023 at 16:05):

something like

Import Ltac2.Std.
Ltac2 hident () := @H.
Ltac2 Notation "tac" arg(list1(constr, ",")) := Std.pattern (List.map (fun x => (x, Std.AllOccurrences)) arg) { on_hyps := Some [(hident (), AllOccurrences, InHyp)] ; on_concl := NoOccurrences }.

Gaëtan Gilbert (Dec 04 2023 at 16:06):

(the auxiliary hident is needed because Ltac2 Notation doesn't like @H, but in practice it should probably not be statically H)

Remy Seassau (Dec 04 2023 at 16:13):

This is exactly what I was looking for, thank you!

Notification Bot (Dec 04 2023 at 16:14):

Remy Seassau has marked this topic as resolved.

Last updated: Oct 12 2024 at 12:01 UTC