Is there a way to give to a Tactic the kind of pattern that one gives to rewrite for instance after a "in", i.e. in particular so that I can pass to the same tactic either an hyp, or
|- * to rewrite in the goal?
A silly self example for concreteness would be:
Axiom f: 1 = 2. Ltac foo := rewrite f. Ltac foo_hyp h := rewrite f in h. Ltac Notation "foo" "in" hyp(h) := foo h.
And the point would be to not need to define
foo that is basically a duplicate of
foo_hyp, but instead do something like:
Axiom f: 1 = 2. Ltac foo_hyp h := rewrite f in h. Ltac Notation "foo" "in" hyp(h) := foo h. Ltac Notation "foo" := foo |-*. (* or "foo goal" or something like that *)
@Yannick Zakowski: the grammar entry to parse
in clauses (the one with
|-) is currently not exported for the purpose of
Tactic Notation. This could be done, like it is done e.g. for
intro_patterns by defining what is called a
genarg and doing mechanically a couple of appropriate changes. The grammar entry is called
Maybe Ltac2 has a ready solution for that otherwise. You should ask @ppedrot.
(edited the topic to keep the answer closer to the question)
Thank you for the answer Hugo!
I will have a look on Ltac2's side, and will alternatively consider opening an issue or a PR as soon as I can, that would be a quite useful feature to have access to.
Let me just mention that Ltac(2) support for this and other "variadic" notations would be a godsend. Quite a few people resort to writing N variants of a tactic — sometimes in a combinatorial explosion.
There is a dedicated type of clauses in Ltac2, as well as its corresponding (primitive) scope.
See for instance the definition of the
set tactic in Ltac2.Notation
Ltac2 Notation "set" p(thunk(pose)) cl(opt(clause)) := Std.set false p (default_on_concl cl).
For true "variadic" tactics, just parse a list instead, and thanks to the magic of datastructures, you should be happy.
Last updated: Oct 03 2023 at 04:02 UTC