The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

This is not possible (and probably won't ever be), but you can do this in Ltac2, see https://coq.inria.fr/refman/proof-engine/ltac2.html#notations  and https://coq.inria.fr/refman/proof-engine/ltac2.html#syntactic-classes , specifically the bit about scope_keys on constr.  I think the syntax is something like

Ltac2 Notation "apply_f" p(constr(my_nat)) := apply '(f $p).

On Tue, Jan 4, 2022, 03:22 Peter LeFanu Lumsdaine <p.l.lumsdaine AT gmail.com> wrote:

Is there a way to give scope annotations to arguments of an Ltac-defined tactic (or a Tactic Notation), so that the argument is always parsed with the specified scope?  I’m looking for something analogous to what you can give for tunctions using [Arguments]:

    Arguments my_function _%nat.

but for tactics.  If I define

    Ltac apply_my_function p := apply (my_function p).

then the argument to [apply_my_function] will *not* automatically be parsed in nat_scope, even though in [apply (my_function p)] it would be.

I’ve tried a few things like

    Tactic Notation "apply_my_function" uconstr(p) := apply (my_function p%nat).

but haven’t found anything that works.

A self-contained MWE for the problem follows below.

Best,

–Peter.

===============
Declare Scope my_nat_scope.
Notation "!1" := Nat.one : my_nat_scope.

Declare Scope my_bool_scope.
Notation "!1" := true : my_bool_scope.

Open Scope my_bool_scope.

Definition f : nat -> nat := fun x => x.
Arguments f _%my_nat.

Check (f !1).

Ltac apply_f p := apply (f p).

Goal nat.
  Fail apply_f !1. (* How to define [apply_f] so that this succeeds? *)
  apply_f !1%my_nat.
Qed.

===============