Stream: Coq users

Topic: Tactic Notation ne_ident_list

view this post on Zulip 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?

view this post on Zulip Jason Gross (Mar 24 2021 at 22:22):

Once 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 => ()
               print_stuff xs)

Ltac foo := ltac2:(lxx |- match ( Ltac1.to_ident) (Ltac1.to_list lxx) with
                          | None => ()
                          | Some xs => print_stuff xs

Tactic Notation "bar" ne_ident_list(lxx) := foo lxx.
Goal True.
  ltac1:(bar a b c).

Last updated: Jun 15 2024 at 05:01 UTC