chore: cleanup

src/Lean/Compiler/IR/Boxing.lean

@@ -316,7 +316,7 @@ partial def visitFnBody : FnBody → M FnBody
 
 def run (env : Environment) (decls : Array Decl) : Array Decl :=
 let ctx : BoxingContext := { decls := decls, env := env }
-let decls := decls.foldl (init := #[]) fun (newDecls : Array Decl) (decl : Decl) =>
+let decls := decls.foldl (init := #[]) fun newDecls decl =>
   match decl with
   | Decl.fdecl f xs t b =>
     let nextIdx  := decl.maxIndex + 1

src/Lean/Compiler/IR/NormIds.lean

@@ -86,7 +86,7 @@ fun m => do
 
 @[inline] def withParams {α : Type} (ps : Array Param) (k : Array Param → N α) : N α :=
 fun m => do
-  let m ← ps.foldlM (init := m) fun (m : IndexRenaming) p => do
+  let m ← ps.foldlM (init := m) fun m p => do
     let n ← getModify fun n => n + 1
     pure $ m.insert p.x.idx n
   let ps := ps.map fun p => { p with x := normVar p.x m }

src/Lean/Compiler/IR/RC.lean

@@ -214,7 +214,8 @@ let liveVars := liveVars.erase z
 (b, liveVars)
 
 def updateVarInfoWithParams (ctx : Context) (ps : Array Param) : Context :=
-let m := ps.foldl (fun (m : VarMap) p => m.insert p.x { ref := p.ty.isObj, consume := !p.borrow }) ctx.varMap
+let m := ps.foldl (init := ctx.varMap) fun m p =>
+  m.insert p.x { ref := p.ty.isObj, consume := !p.borrow }
 { ctx with varMap := m }
 
 partial def visitFnBody : FnBody → Context → (FnBody × LiveVarSet)

src/Lean/Meta/Tactic/Apply.lean

@@ -63,7 +63,7 @@ otherMVars.anyM fun otherMVar =>
     pure $ (otherMVarType.findMVar? fun mvarId => mvarId == mvar.mvarId!).isSome
 
 private def reorderNonDependentFirst (newMVars : Array Expr) : MetaM (List MVarId) := do
-let (nonDeps, deps) ← newMVars.foldlM (init := (#[], #[])) fun (nonDeps, deps) (mvar : Expr) => do
+let (nonDeps, deps) ← newMVars.foldlM (init := (#[], #[])) fun (nonDeps, deps) mvar => do
   let currMVarId := mvar.mvarId!
   if (← dependsOnOthers mvar newMVars) then
     pure (nonDeps, deps.push currMVarId)

src/Lean/Meta/Tactic/Assert.lean

@@ -74,7 +74,7 @@ withMVarContext mvarId $ do
   let xs   := fvarIds.map mkFVar
   let targetNew ← mkForallFVars xs target
   let targetNew := Lean.mkForall userName BinderInfo.default type targetNew
-  let lctxNew := fvarIds.foldl (fun (lctxNew : LocalContext) fvarId => lctxNew.erase fvarId) lctx
+  let lctxNew := fvarIds.foldl (init := lctx) fun lctxNew fvarId => lctxNew.erase fvarId
   let localInstsNew := localInsts.filter fun inst => fvarIds.contains inst.fvar.fvarId!
   let mvarNew ← mkFreshExprMVarAt lctxNew localInstsNew targetNew MetavarKind.syntheticOpaque tag
   let args := (fvarIds.filter fun fvarId => !(lctx.get! fvarId).isLet).map mkFVar

src/Lean/Meta/Tactic/Cases.lean

@@ -166,15 +166,13 @@ else
 private def elimAuxIndices (s₁ : GeneralizeIndicesSubgoal) (s₂ : Array CasesSubgoal) : MetaM (Array CasesSubgoal) :=
 let indicesFVarIds := s₁.indicesFVarIds
 s₂.mapM fun s => do
-  indicesFVarIds.foldlM
-    (fun s indexFVarId =>
-      match s.subst.get indexFVarId with
-      | Expr.fvar indexFVarId' _ =>
-        (do let mvarId ← clear s.mvarId indexFVarId'; pure { s with mvarId := mvarId, subst := s.subst.erase indexFVarId })
-        <|>
-        (pure s)
-      | _ => pure s)
-    s
+  indicesFVarIds.foldlM (init := s) fun s indexFVarId =>
+    match s.subst.get indexFVarId with
+    | Expr.fvar indexFVarId' _ =>
+      (do let mvarId ← clear s.mvarId indexFVarId'; pure { s with mvarId := mvarId, subst := s.subst.erase indexFVarId })
+      <|>
+      (pure s)
+    | _ => pure s
 
 /-
   Convert `s` into an array of `CasesSubgoal`, by attaching the corresponding constructor name,