I want to make a tactic notation that acts something like
eauto with foo. I defined the following
Tactic Notation "foo" ne_ident_list(lxx) := ltac2:(Message.print (Message.of_ident (Ltac1.of_list lxx))).
but I can't seem to figure out how to use the variable
lxx to get my list of identifiers in Ltac2. What ltac2 type does lxx have? Or is there some way to unpack it in Ltac1 and pass the result to Ltac2?
Once https://github.com/coq/coq/pull/13997 is merged, you should be able to do something like
Require Import Ltac2.Ltac2. Require Import Ltac2.Option. Ltac2 rec print_stuff (xs : ident option list) := match xs with |  => () | x :: xs => (match x with | Some x => Message.print (Message.of_ident x) | None => () end; print_stuff xs) end. Ltac foo := ltac2:(lxx |- match Option.map (List.map Ltac1.to_ident) (Ltac1.to_list lxx) with | None => () | Some xs => print_stuff xs end). Tactic Notation "bar" ne_ident_list(lxx) := foo lxx. Goal True. ltac1:(bar a b c).
Last updated: Jan 29 2023 at 05:03 UTC