Tactic Notation ne_ident_list · Coq users

Stream: Coq users

Topic: Tactic Notation ne_ident_list

Gregory Malecha (Mar 23 2021 at 19:57):

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?

Jason Gross (Mar 24 2021 at 22:22):

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: Oct 13 2024 at 01:02 UTC