feat: add code action to generate match cases

[MoritzBeroRoos]

A small adaption of the existing code action for holes in this Situation:

def foo : Expr → Unit := _

gives us a code action that works for

def myfun2 (n:Nat) : Nat :=
  match n

and produces:

def myfun2 (n:Nat) : Nat :=
  match n with
  | .zero => _
  | .succ n => _

[MoritzBeroRoos]

are the underscores in CodeAction.lean a problem? I used this file to put some examples there

[fgdorais]

I'm not sure it's possible but is there a way to add test cases for this?

[MoritzBeroRoos]

I don't know, but i believe not, since i don't see any tests for other code actions. Also since code actions are a vscode feature, existence of any testing automation would be unlikely.

[MoritzBeroRoos]

i have removed the issues with the long lines. It builds locally for me now.
If the build still fails now, i have no idea what it ism the error message from the github log didn't tell me why.

[fgdorais]

You can run lake test and lake lint locally. Looks like some defs are missing docstrings.

[MoritzBeroRoos]

ah good to know.
In this case it's complaining about a missing docstring for the function loop that is declared (via a let) only inside the function findAllInfos.
The outer function (findAllInfos) already has a docstring and i can't actually put a docstring for the inner one (it doesn't parse - expects a term after the := sign).
Can you take a look?

The function is defined at
\Batteries\CodeAction\Misc.lean:290:11

[MoritzBeroRoos]

Thank you, very good fix!
It now builds, tests, and lints locally for me.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch batteries-pr-testing-1307 has successfully built against this PR. (2025-07-05 20:04:43) View Log
• 🟡 Mathlib branch batteries-pr-testing-1307 build against this PR was cancelled. (2025-07-09 23:16:55) View Log
• ✅ Mathlib branch batteries-pr-testing-1307 has successfully built against this PR. (2025-07-10 00:04:19) View Log

[fgdorais]

A few questions and comments:

The full match syntax is described here.

The match syntax supports discriminants that are just terms and also ident : term. Is the latter supported?

Is there a way to support multiple discriminants? That would be helpful since it is time consuming to get all the cases for these.

Is there a reasonable way to support @[match_pattern] declarations? For example, with n : Nat, I would rather obtain

match n with
| 0 => _
| _ + 1 => _

than

match n with
| .zero => _
| .succ _ => _

None of these are deal breakers but they would be great to have.

[MoritzBeroRoos]

Is there a way to support multiple discriminants? That would be helpful since it is time consuming to get all the cases for these.
Would this be the expected ordering for e.g. 2 discriminants?

def myfun2 (n:Nat) (m:Nat): Nat :=
  match n,m with
  | .zero, .zero => 0
  | .zero, .succ m' => 1
  | .succ n', .zero => 2
  | .succ n', .succ m' => 3

[MoritzBeroRoos]

• If i did everything correctly we should now "support" full match syntax (simply ignoring all the additional stuff).

• Multiple discriminants are now supported.

• I have added special support for Nat and List for generation of nicer patterns. In general i don't think there is a way to generate these nice looking patterns automatically. The @[match_pattern] will only specify definitions to be unfolded by the match algorithm, but there is (to me) no clear way to refold this back into the correct thing.

[fgdorais]

This is excellent!

There's an issue with placeholder names:

example (l r : List Nat) : Empty :=
  match l, r with

gives this:

example (l r : List Nat) : Empty :=
  match l, r with
  | [], [] => _
  | [], head :: tail => _
  | head :: tail, [] => _
  | head :: tail, head :: tail => _

This is not valid because head and tail are reused for different matches.

I don't think it's a burden on users to edit the pattern names (they probably will want to do that anyway). But there probably is a better automatic disambiguation solution, especially one that would make it easier to use find/replace instead of manual editing. What do you think?

[fgdorais]

By the way, the CodeAction.Misc file is getting long. It would be great if you could move the match stuff to a CodeAction.Match file.