Metaprogramming MVars for case matching

Stream: lean4

[Reinier van der Gronden]

Hi! I'm currently working on a tactic (to be implemented as editor suggestions later) that attempts to auto-complete cases and induction statements, with some extra bells and whistles. My current implementation already produces in the (very trivial) example:

example (n : Nat) : n = n := by
  myTactic induction n
  -- suggests
  induction n with
  | zero => sorry
  | succ n_1 n_1.ih => sorry

For some other suggestions and improvements I want to make, I need access to the state/MVarId at the start of the case block in the inductionAlt (before execution of either sorry). Is there a canonical way of getting these mvars, given the MVarId prior to the cases? Note that we can't seem to use the cases without the match statement, because then we don't get the goals with their declarations named as in succ n_1.

[Reinier van der Gronden]

Small bump in case some people missed this over the weekend :sweat_smile:

[James Gallicchio]

(I don't know how to answer your question, but are you working towards something like agda's split on variable? That'd be so helpful :0)

[Reinier van der Gronden]

are you working towards something like agda's split on variable?

While I'm not familiar with Agda specifically, I believe it should work similarly. The only caveat is that in its current form it's a manual operation (e.g. write myTactic induction n, then copy and paste the suggestion from the infoview). I believe in this RFC people are working on actually implementing a system where these code suggestions can be automated for the user, but for now that's not the case, sadly.