Writing a tactic macro with different syntax categories

Stream: new members

[Josh Cohen]

I want to write a tactic macro that looks something like:

syntax "foo" Lean.Parser.Tactic.elimTarget Lean.Parser.Tactic.elimTarget  : tactic
macro_rules
  | `(tactic|foo $e1:elimTarget $e2:elimTarget) =>
  `(tactic| induction $e1 generalizing $e2 <;> cases $e2)

That is, I have two arguments which will both be instances of some inductive type, and I want to do case analysis in a particular order. However, Lean does not like the generalizing $e2, since it expects term syntax rather than Lean.Parser.Tactic.elimTarget. Is there a way to treat elimTarget as a term? Or how else could I resolve this? Thanks

[Kyle Miller]

What do you want it to do with full elimTarget syntax? Remember that it's either a term e or of the form h : e, and also generalizing only supports references to local variables.

Perhaps this is sufficient for your use case?

syntax "foo" ident ident  : tactic
macro_rules
  | `(tactic|foo $e1:ident $e2:ident) =>
  `(tactic| induction $e1:ident generalizing $e2:ident <;> cases $e2:ident)

If you want terms, you can upgrade ident to term (useful if you want to refer to a local variable using ‹T› syntax), but note that you'll need to adjust the syntax by for example adding a ", " into it between the terms or increasing the precedence to term:max.

[Josh Cohen]

Thanks, that was exactly what I needed. I wasn't specifically trying to use elimTarget, I only changed that following type errors when using term.