From a915822454e666f2df15f87172aa77ff3c67b85f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 17 Oct 2020 13:49:14 -0700
Subject: [PATCH] chore: cleanup

---
 src/Lean/Compiler/IR/Boxing.lean  |  2 +-
 src/Lean/Compiler/IR/NormIds.lean |  2 +-
 src/Lean/Compiler/IR/RC.lean      |  3 ++-
 src/Lean/Meta/Tactic/Apply.lean   |  2 +-
 src/Lean/Meta/Tactic/Assert.lean  |  2 +-
 src/Lean/Meta/Tactic/Cases.lean   | 16 +++++++---------
 6 files changed, 13 insertions(+), 14 deletions(-)

diff --git a/src/Lean/Compiler/IR/Boxing.lean b/src/Lean/Compiler/IR/Boxing.lean
index 8755a80609..da971aa225 100644
--- a/src/Lean/Compiler/IR/Boxing.lean
+++ b/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
diff --git a/src/Lean/Compiler/IR/NormIds.lean b/src/Lean/Compiler/IR/NormIds.lean
index d0f98b891c..ace145d24e 100644
--- a/src/Lean/Compiler/IR/NormIds.lean
+++ b/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 }
diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean
index b5f733e65b..1fa39d2190 100644
--- a/src/Lean/Compiler/IR/RC.lean
+++ b/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)
diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean
index bb77316e87..afab5c9aa8 100644
--- a/src/Lean/Meta/Tactic/Apply.lean
+++ b/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)
diff --git a/src/Lean/Meta/Tactic/Assert.lean b/src/Lean/Meta/Tactic/Assert.lean
index 4046bbe276..75a88a9bfd 100644
--- a/src/Lean/Meta/Tactic/Assert.lean
+++ b/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
diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean
index fa89148895..61f389510f 100644
--- a/src/Lean/Meta/Tactic/Cases.lean
+++ b/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,