refactor: Add MkMatcherInput.

Since we are going to make `mkMatcher` reversible, it's quite useful to have the input be a `structure`. This way we make sure, that the inverse function always returns the same type as `mkMatcher` needs as input.

src/Lean/Elab/Match.lean

@@ -941,8 +941,8 @@ where
     let wildcards := mkArray num hole
     return altViews.map fun altView => { altView with patterns := wildcards ++ altView.patterns }
 
-def mkMatcher (elimName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss : List AltLHS) : TermElabM MatcherResult :=
-  Meta.Match.mkMatcher elimName matchType numDiscrs lhss
+def mkMatcher (input : Meta.Match.MkMatcherInput) : TermElabM MatcherResult :=
+  Meta.Match.mkMatcher input
 
 register_builtin_option match.ignoreUnusedAlts : Bool := {
   defValue := false
@@ -1044,7 +1044,7 @@ private def elabMatchAux (generalizing? : Option Bool) (discrStxs : Array Syntax
   else
     let numDiscrs := discrs.size
     let matcherName ← mkAuxName `match
-    let matcherResult ← mkMatcher matcherName matchType numDiscrs altLHSS
+    let matcherResult ← mkMatcher { matcherName, matchType, numDiscrs, lhss := altLHSS }
     let motive ← forallBoundedTelescope matchType numDiscrs fun xs matchType => mkLambdaFVars xs matchType
     reportMatcherResultErrors altLHSS matcherResult
     let r := mkApp matcherResult.matcher motive

src/Lean/Meta/Match/Match.lean

@@ -700,6 +700,13 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (B
     modifyEnv fun env => matcherExt.modifyState env fun s => s.insert (result.value, compile) name
     return (true, mkAppN (mkConst name result.levelArgs.toList) result.exprArgs)
 
+
+structure MkMatcherInput where
+  matcherName : Name 
+  matchType : Expr
+  numDiscrs : Nat
+  lhss : List Match.AltLHS
+
 /-
 Create a dependent matcher for `matchType` where `matchType` is of the form
 `(a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> B[a_1, ..., a_n]`
@@ -709,7 +716,8 @@ The number of patterns must be the same in each `AltLHS`.
 The generated matcher has the structure described at `MatcherInfo`. The motive argument is of the form
 `(motive : (a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> Sort v)`
 where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition. -/
-def mkMatcher (matcherName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss : List AltLHS) : MetaM MatcherResult :=
+def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult :=
+  let ⟨matcherName, matchType, numDiscrs, lhss⟩ := input
   forallBoundedTelescope matchType numDiscrs fun majors matchTypeBody => do
   checkNumPatterns majors lhss
   /- We generate an matcher that can eliminate using different motives with different universe levels.

tests/lean/run/depElim1.lean

@@ -160,7 +160,7 @@ def mkTester (elimName : Name) (majors : List Expr) (lhss : List AltLHS) (inProp
 generalizeTelescope majors.toArray fun majors => do
   let resultType := if inProp then mkConst `True /- some proposition -/ else mkConst `Nat
   let matchType ← mkForallFVars majors resultType
-  Match.mkMatcher elimName matchType majors.size lhss
+  Match.mkMatcher { matcherName := elimName, matchType, numDiscrs := majors.size, lhss }
 
 def test (ex : Name) (numPats : Nat) (elimName : Name) (inProp : Bool := false) : MetaM Unit :=
 withDepElimFrom ex numPats fun majors alts => do