Sometimes it is necessary to convert an `Ltac`

to a `Tactic Notation`

, e.g. when one needs an argument to be parsed a certain way and ltac doesn't provide another way of forcing the right parsing (see https://github.com/coq/coq/issues/18111).

But which parsing "category" do I need to set for general ltac terms / ltac thunks? Let's say I have a tactic like this

```
Ltac run_tac tac := tac ().
```

How do I make that a notation? I tried this but it doesn't work:

```
Ltac run_tac tac := tac ().
Tactic Notation "run_tac2" tactic(tac) := tac.
Goal forall n : nat, True.
Proof.
intros n.
run_tac ltac:(fun _ => destruct n as [|n']).
Undo.
run_tac2 ltac:(fun _ => destruct n as [|n']).
(* Error: An unnamed user-defined tactic was not fully applied: There is a missing argument for variable _,
no arguments at all were provided. *)
```

I've looked through the table at https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#coq:cmd.Tactic-Notation but none of the categories seem to fit

but also the table is incomplete, e.g. `open_constr`

is missing, so maybe there are other things missing as well

I am not sure I understand the question. You are passing an ltac `fun`

to both `run_tac`

and `run_tac2`

but only `run_tac`

actually supplies the unit argument. If you change `run_tac2`

to `tac ()`

it seems to work.

You can also use `ltac:(idtac; ..)`

to thunk tactics and that way you can skip `fun _ =>`

and the unit argument

do you actually need thunk/`idtac`

for tactics passed to `Tactic Notation`

? The stdpp tactics don't seem to

```
Tactic Notation "run_tac2" tactic(tac) := tac.
```

beware`tactic`

is probably almost always the wrong precedence, `run_tac2 a; b; c`

would parse as `run_tac2 (a; b; c)`

.

You have `tactic0`

to `tactic4`

, matching `ltac_expr0`

to `ltac_expr4`

in the ltac grammar: https://coq.inria.fr/refman/proof-engine/ltac.html#syntax. I've recommended `tactic3`

in the past for stdpp, but I suspect `tactic1`

would make more sense.

Janno said:

I am not sure I understand the question. You are passing an ltac

`fun`

to both`run_tac`

and`run_tac2`

but only`run_tac`

actually supplies the unit argument. If you change`run_tac2`

to`tac ()`

it seems to work.

oh I am stupid, you are right.

I had some very strange trouble porting an existing `Ltac`

to a `Tactic Notation`

that lead to the same error and then made this fatal mistake while minimizing...

I wonder now if my original issue was a similar typo or something deeper. sadly the error doesn't say *where* arguments failed to be provided.

Paolo Giarrusso said:

You have

`tactic0`

to`tactic4`

, matching`ltac_expr0`

to`ltac_expr4`

in the ltac grammar: https://coq.inria.fr/refman/proof-engine/ltac.html#syntax. I've recommended`tactic3`

in the past for stdpp, but I suspect`tactic1`

would make more sense.

yeah I know, this is just for demonstration. I never know which number to pick, I just know the default is bad...

Paolo Giarrusso said:

do you actually need thunk/

`idtac`

for tactics passed to`Tactic Notation`

? The stdpp tactics don't seem to

probably not but we always use thunks since it is the only way to be sure

There's at least no visible thunking with `naive_solver eauto with foo`

.

All tactic arguments are delayed by default unless they are headed by match, lazymatch, multimatch, or let

Paolo Giarrusso said:

There's at least no visible thunking with

`naive_solver eauto with foo`

.

ah sure yes we avoid the thunks to get a nicer UI. I meant in the implementation. we have to use CPS for tons of stuff anyway so the few additional closures for thunking barely stick out^^

Last updated: Jun 23 2024 at 05:02 UTC