The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

There are two ways to do this:

1. Write a "dependently typed" tactic that takes a `nat` encoding how many arguments it expects, e.g.,

Ltac myintros_then n k :=
  lazymatch n with
  | O => k ()
  | S ?n
    => fun H
       => myintros_then n ltac:(fun _ => k (); intro H)
  end.
Ltac myintros n := myintros_then n ltac:(fun _ => idtac).
Goal True -> True -> True -> True.
  myintros 3 A B C.

2. Use Tactic Notation, like

Tactic Notation "myintros" ident_list(vars) := intros vars.

Goal True -> True -> True -> True.
  myintros A B C.

Note that, unfortunately, there's not really a way to manipulate lists of things in Ltac, which brings us to

3. Use Ltac2, like

Require Import Ltac2.Ltac2.
Ltac2 Notation "myintros" p(intropatterns) := intros0 false p.

Goal True -> True -> True -> True.
  myintros A B C.

On Tue, Aug 18, 2020 at 10:35 PM Christopher Ernest Sally <christopherernestsally AT gmail.com> wrote:

Hello Club

I'm looking to write variadic tactics ala clear, intros, destruct but inside coq, rather than ML.

I wanted to ask what was the best known methodology for this currently.

Thanks

Chris