chore: cleanup

src/Lean/Elab/Tactic/Induction.lean

@@ -102,7 +102,7 @@ structure Result where
   Remark: the method `addImplicitTargets` may be used to compute the sequence of implicit and explicit targets
   from the explicit ones.
 -/
-partial def mkElimApp (elimName : Name) (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name) : TermElabM Result := do
+partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name) : TermElabM Result := do
   let rec loop : M Unit := do
     match (← getFType) with
     | Expr.forallE binderName _ _ c =>
@@ -115,7 +115,7 @@ partial def mkElimApp (elimName : Name) (elimInfo : ElimInfo) (targets : Array E
         let s ← get
         let ctx ← read
         unless s.targetPos < ctx.targets.size do
-          throwError "insufficient number of targets for '{elimName}'"
+          throwError "insufficient number of targets for '{elimInfo.name}'"
         let target := ctx.targets[s.targetPos]
         let expectedType ← getArgExpectedType
         let target ← withConfig (fun cfg => { cfg with assignSyntheticOpaque := true }) do Term.ensureHasType expectedType target
@@ -140,7 +140,7 @@ partial def mkElimApp (elimName : Name) (elimInfo : ElimInfo) (targets : Array E
       loop
     | _ =>
       pure ()
-  let f ← Term.mkConst elimName
+  let f ← Term.mkConst elimInfo.name
   let fType ← inferType f
   let (_, s) ← (loop).run { elimInfo := elimInfo, targets := targets } |>.run { f := f, fType := fType }
   let mut others := #[]
@@ -391,7 +391,7 @@ def getInductiveValFromMajor (major : Expr) : TacticM InductiveVal :=
       (fun val _ => pure val)
 
 -- `optElimId` is of the form `("using" ident)?`
-private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (induction : Bool): TacticM (Name × ElimInfo) := do
+private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (induction : Bool): TacticM ElimInfo := do
   if optElimId.isNone then
     unless targets.size == 1 do
       throwError "eliminator must be provided when multiple targets are used (use 'using <eliminator-name>')"
@@ -401,11 +401,11 @@ private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (inducti
     if induction && indVal.isNested then
       throwError "'induction' tactic does not support nested inductive types, the eliminator '{mkRecName indVal.name}' has multiple motives"
     let elimName := if induction then mkRecName indVal.name else mkCasesOnName indVal.name
-    return (elimName, ← getElimInfo elimName)
+    getElimInfo elimName
   else
     let elimId := optElimId[1]
     let elimName ← withRef elimId do resolveGlobalConstNoOverloadWithInfo elimId
-    return (elimName, ← withRef elimId do getElimInfo elimName)
+    withRef elimId <| getElimInfo elimName
 
 private def shouldGeneralizeTarget (e : Expr) : MetaM Bool := do
   if let .fvar fvarId .. := e then
@@ -426,7 +426,7 @@ private def generalizeTargets (exprs : Array Expr) : TacticM (Array Expr) := do
   let alts := getAltsOfOptInductionAlts optInductionAlts
   let targets ← withMainContext <| stx[1].getSepArgs.mapM (elabTerm · none)
   let targets ← generalizeTargets targets
-  let (elimName, elimInfo) ← getElimNameInfo stx[2] targets (induction := true)
+  let elimInfo ← getElimNameInfo stx[2] targets (induction := true)
   let mvarId ← getMainGoal
   -- save initial info before main goal is reassigned
   let initInfo ← mkTacticInfo (← getMCtx) (← getUnsolvedGoals) (← getRef)
@@ -485,14 +485,14 @@ def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr) :=
   let optPreTac := getOptPreTacOfOptInductionAlts optInductionAlts
   let alts :=  getAltsOfOptInductionAlts optInductionAlts
   let targetRef := stx[1]
-  let (elimName, elimInfo) ← getElimNameInfo stx[2] targets (induction := false)
+  let elimInfo ← getElimNameInfo stx[2] targets (induction := false)
   let mvarId ← getMainGoal
   -- save initial info before main goal is reassigned
   let initInfo ← mkTacticInfo (← getMCtx) (← getUnsolvedGoals) (← getRef)
   let tag ← getMVarTag mvarId
   withMVarContext mvarId do
     let targets ← addImplicitTargets elimInfo targets
-    let result ← withRef targetRef <| ElimApp.mkElimApp elimName elimInfo targets tag
+    let result ← withRef targetRef <| ElimApp.mkElimApp elimInfo targets tag
     let elimArgs := result.elimApp.getAppArgs
     let targets ← elimInfo.targetsPos.mapM fun i => instantiateMVars elimArgs[i]
     let motiveType ← inferType elimArgs[elimInfo.motivePos]
@@ -507,5 +507,4 @@ builtin_initialize
   registerTraceClass `Elab.cases
   registerTraceClass `Elab.induction
 
-
 end Lean.Elab.Tactic