From 2d2d39c78e15542fc1b67ff6600ee01038304d79 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 7 Nov 2020 17:27:57 -0800
Subject: [PATCH] chore: use `mut`

---
 src/Init/Data/Array/Basic.lean              |  8 ++---
 src/Init/Data/Array/Subarray.lean           |  2 +-
 src/Init/LeanInit.lean                      | 10 +++---
 src/Lean/Compiler/ExternAttr.lean           |  2 +-
 src/Lean/Compiler/IR/Basic.lean             |  2 +-
 src/Lean/Compiler/IR/Boxing.lean            |  6 ++--
 src/Lean/Compiler/IR/Format.lean            |  2 +-
 src/Lean/Compiler/IR/SimpCase.lean          |  6 ++--
 src/Lean/Data/Format.lean                   |  4 +--
 src/Lean/Delaborator.lean                   |  2 +-
 src/Lean/Elab/App.lean                      | 10 +++---
 src/Lean/Elab/Attributes.lean               |  4 +--
 src/Lean/Elab/Binders.lean                  |  2 +-
 src/Lean/Elab/BuiltinNotation.lean          |  8 +++--
 src/Lean/Elab/Declaration.lean              |  8 ++---
 src/Lean/Elab/Do.lean                       |  4 +--
 src/Lean/Elab/Level.lean                    |  4 +--
 src/Lean/Elab/Match.lean                    | 23 +++++++-------
 src/Lean/Elab/MutualDef.lean                | 10 +++---
 src/Lean/Elab/PreDefinition/Basic.lean      |  2 +-
 src/Lean/Elab/PreDefinition/Structural.lean |  8 ++---
 src/Lean/Elab/Print.lean                    |  6 ++--
 src/Lean/Elab/StructInst.lean               |  2 +-
 src/Lean/Elab/Syntax.lean                   |  2 +-
 src/Lean/Elab/Tactic/Basic.lean             |  6 ++--
 src/Lean/Elab/Tactic/Generalize.lean        |  2 +-
 src/Lean/Elab/Tactic/Induction.lean         | 34 ++++++++++-----------
 src/Lean/Elab/Tactic/Rewrite.lean           |  2 +-
 src/Lean/Environment.lean                   | 10 +++---
 src/Lean/Meta/AbstractNestedProofs.lean     |  2 +-
 src/Lean/Meta/FunInfo.lean                  |  2 +-
 src/Lean/Meta/InferType.lean                |  8 ++---
 src/Lean/Meta/LevelDefEq.lean               |  2 +-
 src/Lean/Meta/Match/Match.lean              |  2 +-
 src/Lean/Meta/RecursorInfo.lean             | 10 +++---
 src/Lean/Meta/Reduce.lean                   |  2 +-
 src/Lean/Meta/SynthInstance.lean            |  2 +-
 src/Lean/Meta/Tactic/Apply.lean             |  2 +-
 src/Lean/Meta/Tactic/ElimInfo.lean          |  2 +-
 src/Lean/Meta/Tactic/Induction.lean         |  4 +--
 src/Lean/Meta/WHNF.lean                     |  8 ++---
 src/Lean/MetavarContext.lean                |  2 +-
 src/Lean/Parser/Transform.lean              |  2 +-
 src/Lean/ParserCompiler.lean                |  4 +--
 src/Std/Data/PersistentArray.lean           |  3 +-
 45 files changed, 126 insertions(+), 122 deletions(-)

diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 672b789825..d7f1cda12b 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -171,7 +171,7 @@ def modifyM {m : Type u → Type v} [Monad m] [Inhabited α] (a : Array α) (i :
     let idx : Fin a.size := ⟨i, h⟩
     let v                := a.get idx
     let a                := a.set idx (arbitrary α)
-    v ← f v
+    let v ← f v
     pure $ (a.set idx v)
   else
     pure a
@@ -343,7 +343,7 @@ def findM? {α : Type} {m : Type → Type} [Monad m] (as : Array α) (p : α →
 
 @[inline]
 def findIdxM? {m : Type → Type u} [Monad m] (as : Array α) (p : α → m Bool) : m (Option Nat) := do
-  let i := 0
+  let mut i := 0
   for a in as do
     if (← p a) then
       return i
@@ -599,8 +599,8 @@ def getMax? {α : Type u} (as : Array α) (lt : α → α → Bool) : Option α
 
 @[inline]
 def partition {α : Type u} (p : α → Bool) (as : Array α) : Array α × Array α := do
-  let bs := #[]
-  let cs := #[]
+  let mut bs := #[]
+  let mut cs := #[]
   for a in as do
     if p a then
       bs := bs.push a
diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean
index b885d17863..3e9db469aa 100644
--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@@ -92,7 +92,7 @@ def toSubarray (as : Array α) (start stop : Nat) : Subarray α :=
        { as := as, start := as.size, stop := as.size, h₁ := Nat.leRefl _, h₂ := Nat.leRefl _ }
 
 def ofSubarray (s : Subarray α) : Array α := do
-  let as := mkEmpty (s.stop - s.start)
+  let mut as := mkEmpty (s.stop - s.start)
   for a in s do
     as := as.push a
   return as
diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean
index ef422d43d7..d5bb9d0eec 100644
--- a/src/Init/LeanInit.lean
+++ b/src/Init/LeanInit.lean
@@ -568,8 +568,8 @@ def mkIdent (val : Name) : Syntax :=
   Syntax.node nullKind args
 
 def mkSepArray (as : Array Syntax) (sep : Syntax) : Array Syntax := do
-  let i := 0
-  let r := #[]
+  let mut i := 0
+  let mut r := #[]
   for a in as do
     if i > 0 then
       r := r.push sep $.push a
@@ -913,7 +913,7 @@ private partial def mapSepElemsMAux {m : Type → Type} [Monad m] (a : Array Syn
   if h : i < a.size then
     let stx := a.get ⟨i, h⟩
     if i % 2 == 0 then do
-      stx ← f stx
+      let stx ← f stx
       mapSepElemsMAux a f (i+1) (acc.push stx)
     else
       mapSepElemsMAux a f (i+1) (acc.push stx)
@@ -968,8 +968,8 @@ partial def isInterpolatedStrLit? (stx : Syntax) : Option String :=
   | some val => decodeInterpStrLit val
 
 def expandInterpolatedStrChunks (chunks : Array Syntax) (mkAppend : Syntax → Syntax → MacroM Syntax) (mkElem : Syntax → MacroM Syntax) : MacroM Syntax := do
-  let i      := 0
-  let result := Syntax.missing
+  let mut i := 0
+  let mut result := Syntax.missing
   for elem in chunks do
     let elem ← match elem.isInterpolatedStrLit? with
       | none     => mkElem elem
diff --git a/src/Lean/Compiler/ExternAttr.lean b/src/Lean/Compiler/ExternAttr.lean
index 81d9b554da..b67206dcc7 100644
--- a/src/Lean/Compiler/ExternAttr.lean
+++ b/src/Lean/Compiler/ExternAttr.lean
@@ -84,7 +84,7 @@ builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
     descr := "builtin and foreign functions",
     getParam := fun _ stx => ofExcept $ syntaxToExternAttrData stx,
     afterSet := fun declName _ => do
-      let env ← getEnv
+      let mut env ← getEnv
       if env.isProjectionFn declName || env.isConstructor declName then do
         env ← ofExcept $ addExtern env declName
         setEnv env
diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean
index 25d100ec5a..07db6ac494 100644
--- a/src/Lean/Compiler/IR/Basic.lean
+++ b/src/Lean/Compiler/IR/Basic.lean
@@ -545,7 +545,7 @@ def addParamsRename (ρ : IndexRenaming) (ps₁ ps₂ : Array Param) : Option In
   if ps₁.size != ps₂.size then
     none
   else
-    let ρ := ρ
+    let mut ρ := ρ
     for i in [:ps₁.size] do
       ρ ← addParamRename ρ ps₁[i] ps₂[i]
     pure ρ
diff --git a/src/Lean/Compiler/IR/Boxing.lean b/src/Lean/Compiler/IR/Boxing.lean
index 3111223545..ca98e3a435 100644
--- a/src/Lean/Compiler/IR/Boxing.lean
+++ b/src/Lean/Compiler/IR/Boxing.lean
@@ -224,9 +224,9 @@ def mkCast (x : VarId) (xType : IRType) (expectedType : IRType) : M Expr := do
   | _         => k x
 
 @[specialize] def castArgsIfNeededAux (xs : Array Arg) (typeFromIdx : Nat → IRType) : M (Array Arg × Array FnBody) := do
-  let xs' := #[]
-  let bs  := #[]
-  let i   := 0
+  let mut xs' := #[]
+  let mut bs  := #[]
+  let mut i   := 0
   for x in xs do
     let expected := typeFromIdx i
     match x with
diff --git a/src/Lean/Compiler/IR/Format.lean b/src/Lean/Compiler/IR/Format.lean
index 03c2ed6dcf..1645751fce 100644
--- a/src/Lean/Compiler/IR/Format.lean
+++ b/src/Lean/Compiler/IR/Format.lean
@@ -26,7 +26,7 @@ instance : ToFormat LitVal := ⟨formatLitVal⟩
 
 private def formatCtorInfo : CtorInfo → Format
   | { name := name, cidx := cidx, usize := usize, ssize := ssize, .. } => do
-    let r := f!"ctor_{cidx}"
+    let mut r := f!"ctor_{cidx}"
     if usize > 0 || ssize > 0 then
       r := f!"{r}.{usize}.{ssize}"
     if name != Name.anonymous then
diff --git a/src/Lean/Compiler/IR/SimpCase.lean b/src/Lean/Compiler/IR/SimpCase.lean
index c75cf0ea1e..0560ebdadd 100644
--- a/src/Lean/Compiler/IR/SimpCase.lean
+++ b/src/Lean/Compiler/IR/SimpCase.lean
@@ -18,15 +18,15 @@ def ensureHasDefault (alts : Array Alt) : Array Alt :=
 
 private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := do
   let aBody := (alts.get! i).body
-  let n := 1
+  let mut n := 1
   for j in [i+1:alts.size] do
     if alts[j].body == aBody then
       n := n+1
   return n
 
 private def maxOccs (alts : Array Alt) : Alt × Nat := do
-  let maxAlt := alts[0]
-  let max    := getOccsOf alts 0
+  let mut maxAlt := alts[0]
+  let mut max    := getOccsOf alts 0
   for i in [1:alts.size] do
     let curr := getOccsOf alts i
     if curr > max then
diff --git a/src/Lean/Data/Format.lean b/src/Lean/Data/Format.lean
index e9eb24d841..7d3ae256b4 100644
--- a/src/Lean/Data/Format.lean
+++ b/src/Lean/Data/Format.lean
@@ -245,8 +245,8 @@ instance {α : Type u} {β : Type v} [ToFormat α] [ToFormat β] : ToFormat (Pro
 ⟩
 
 def Format.joinArraySep {α : Type u} [ToFormat α] (as : Array α) (sep : Format) : Format := do
-  let r := nil
-  let i := 0
+  let mut r := nil
+  let mut i := 0
   for a in as do
     if i > 0 then
       r := r ++ sep ++ format a
diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index f6196e1f4a..1c0cd012b7 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -378,7 +378,7 @@ def delabAppImplicit : Delab := whenNotPPOption getPPExplicit do
 def delabMData : Delab := do
   -- only interpret `pp.` values by default
   let Expr.mdata m _ _ ← getExpr | unreachable!
-  let posOpts := (← read).optionsPerPos
+  let mut posOpts := (← read).optionsPerPos
   let pos := (← read).pos
   for (k, v) in m do
     if (`pp).isPrefixOf k then
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index bc8e3209b2..1f4b77aa0f 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -292,8 +292,8 @@ private def addEtaArg (k : M Expr) : M Expr := do
 /- This method execute after all application arguments have been processed. -/
 private def finalize : M Expr := do
   let s ← get
-  let e     := s.f
-  let eType := s.fType
+  let mut e     := s.f
+  let mut eType := s.fType
   -- all user explicit arguments have been consumed
   trace[Elab.app.finalize]! e
   let ref ← getRef
@@ -572,7 +572,7 @@ private partial def mkBaseProjections (baseStructName : Name) (structName : Name
   match getPathToBaseStructure? env baseStructName structName with
   | none => throwError "failed to access field in parent structure"
   | some path =>
-    let e := e
+    let mut e := e
     for projFunName in path do
       let projFn ← mkConst projFunName
       e ← elabAppArgs projFn #[{ name := `self, val := Arg.expr e }] (args := #[]) (expectedType? := none) (explicit := false) (ellipsis := false)
@@ -584,8 +584,8 @@ private partial def mkBaseProjections (baseStructName : Name) (structName : Name
 private def addLValArg (baseName : Name) (fullName : Name) (e : Expr) (args : Array Arg) (namedArgs : Array NamedArg) (fType : Expr)
     : TermElabM (Array Arg) :=
   forallTelescopeReducing fType fun xs _ => do
-    let i         := 0
-    let namedArgs := namedArgs
+    let mut i := 0
+    let mut namedArgs := namedArgs
     for x in xs do
       let xDecl ← getLocalDecl x.fvarId!
       if xDecl.binderInfo.isExplicit then
diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean
index 3c94236785..20a0588dd9 100644
--- a/src/Lean/Elab/Attributes.lean
+++ b/src/Lean/Elab/Attributes.lean
@@ -24,7 +24,7 @@ def elabAttr {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [Add
     | some str => pure $ mkNameSimple str
   unless isAttribute (← getEnv) attrName do
     throwError! "unknown attribute [{attrName}]"
-  let args := stx[1]
+  let mut args := stx[1]
   -- the old frontend passes Syntax.missing for empty args, for reasons
   if args.getNumArgs == 0 then
     args := Syntax.missing
@@ -32,7 +32,7 @@ def elabAttr {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [Add
 
 -- sepBy1 attrInstance ", "
 def elabAttrs {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (stx : Syntax) : m (Array Attribute) := do
-  let attrs := #[]
+  let mut attrs := #[]
   for attr in stx.getSepArgs do
     attrs := attrs.push (← elabAttr attr)
   return attrs
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 8648fd8cc2..32eb08e75c 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -44,7 +44,7 @@ partial def quoteAutoTactic : Syntax → TermElabM Syntax
     if stx.isAntiquot then
       throwErrorAt stx "invalic auto tactic, antiquotation is not allowed"
     else
-      let quotedArgs ← `(Array.empty)
+      let mut quotedArgs ← `(Array.empty)
       for arg in args do
         if k == nullKind && Quotation.isAntiquotSplice arg then
           throwErrorAt arg "invalic auto tactic, antiquotation is not allowed"
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index be9126065d..289f140108 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -361,16 +361,18 @@ private def elabCDot (stx : Syntax) (expectedType? : Option Expr) : TermElabM Ex
   let expectedType ← tryPostponeIfHasMVars expectedType? "invalid `▸` notation"
   match_syntax stx with
   | `($heq ▸ $h) => do
-     let heq ← elabTerm heq none
+     let mut heq ← elabTerm heq none
      let heqType ← inferType heq
      let heqType ← instantiateMVars heqType
      match (← Meta.matchEq? heqType) with
      | none => throwError! "invalid `▸` notation, argument{indentExpr heq}\nhas type{indentExpr heqType}\nequality expected"
      | some (α, lhs, rhs) =>
+       let mut lhs := lhs
+       let mut rhs := rhs
        let mkMotive (typeWithLooseBVar : Expr) :=
          withLocalDeclD (← mkFreshUserName `x) α fun x => do
            mkLambdaFVars #[x] $ typeWithLooseBVar.instantiate1 x
-       let expectedAbst ← kabstract expectedType rhs
+       let mut expectedAbst ← kabstract expectedType rhs
        unless expectedAbst.hasLooseBVars do
          expectedAbst ← kabstract expectedType lhs
          unless expectedAbst.hasLooseBVars do
@@ -397,7 +399,7 @@ private def elabCDot (stx : Syntax) (expectedType? : Option Expr) : TermElabM Ex
 
 @[builtinTermElab stateRefT] def elabStateRefT : TermElab := fun stx _ => do
   let σ ← elabType stx[1]
-  let m := stx[2]
+  let mut m := stx[2]
   if m.getKind == `Lean.Parser.Term.macroDollarArg then
     m := m[1]
   let m ← elabTerm m (← mkArrow (mkSort levelOne) (mkSort levelOne))
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 3f6217d6b1..b0aabfb5fd 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -202,8 +202,8 @@ private partial def splitMutualPreamble (elems : Array Syntax) : Option (Array S
 
 @[builtinMacro Lean.Parser.Command.mutual]
 def expandMutualNamespace : Macro := fun stx => do
-  let ns?      := none
-  let elemsNew := #[]
+  let mut ns?      := none
+  let mut elemsNew := #[]
   for elem in stx[1].getArgs do
     match ns?, expandDeclNamespace? elem with
     | _, none                         => elemsNew := elemsNew.push elem
@@ -222,8 +222,8 @@ def expandMutualNamespace : Macro := fun stx => do
 
 @[builtinMacro Lean.Parser.Command.mutual]
 def expandMutualElement : Macro := fun stx => do
-  let elemsNew := #[]
-  let modified := false
+  let mut elemsNew := #[]
+  let mut modified := false
   for elem in stx[1].getArgs do
     match (← expandMacro? elem) with
     | some elemNew => elemsNew := elemsNew.push elemNew; modified := true
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 3959c7e00f..a25a50db60 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -573,7 +573,7 @@ def getDoLetRecVars (doLetRec : Syntax) : TermElabM (Array Name) := do
   -- letRecDecls is an array of `(group (optional attributes >> letDecl))`
   let letRecDecls := doLetRec[1].getSepArgs
   let letDecls := letRecDecls.map fun p => p[1]
-  let allVars := #[]
+  let mut allVars := #[]
   for letDecl in letDecls do
     let vars ← getLetDeclVars letDecl
     allVars := allVars ++ vars
@@ -1007,7 +1007,7 @@ partial def toTerm : Code → M Syntax
   | Code.seq stx k          => do seqToTerm stx (← toTerm k)
   | Code.ite ref _ o c t e  => do pure $ mkIte ref o c (← toTerm t) (← toTerm e)
   | Code.«match» ref discrs optType alts => do
-    let termSepAlts := #[]
+    let mut termSepAlts := #[]
     for alt in alts do
       termSepAlts := termSepAlts.push $ mkAtomFrom alt.ref "|"
       let rhs ← toTerm alt.rhs
diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean
index 4e0a0d43c1..5c9cb61aaf 100644
--- a/src/Lean/Elab/Level.lean
+++ b/src/Lean/Elab/Level.lean
@@ -44,14 +44,14 @@ partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do
     elabLevel (stx.getArg 1)
   else if kind == `Lean.Parser.Level.max then
     let args := stx.getArg 1 $.getArgs
-    let lvl ← elabLevel args.back
+    let mut lvl ← elabLevel args.back
     for arg in args[:args.size-1] do
       let arg ← elabLevel arg
       lvl := mkLevelMax lvl arg
     return lvl
   else if kind == `Lean.Parser.Level.imax then
     let args := stx.getArg 1 $.getArgs
-    let lvl ← elabLevel args.back
+    let mut lvl ← elabLevel args.back
     for arg in args[:args.size-1] do
       let arg ← elabLevel arg
       lvl := mkLevelIMax lvl arg
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 29c2262355..af46761440 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -49,9 +49,9 @@ private def expandSimpleMatchWithType (stx discr lhsVar type rhs : Syntax) (expe
   withMacroExpansion stx newStx $ elabTerm newStx expectedType?
 
 private def elabDiscrsWitMatchType (discrStxs : Array Syntax) (matchType : Expr) (expectedType : Expr) : TermElabM (Array Expr) := do
-  let discrs := #[]
-  let i := 0
-  let matchType := matchType
+  let mut discrs := #[]
+  let mut i := 0
+  let mut matchType := matchType
   for discrStx in discrStxs do
     i := i + 1
     matchType ← whnf matchType
@@ -134,10 +134,11 @@ def expandMacrosInPatterns (matchAlts : Array MatchAltView) : MacroM (Array Matc
   private def getMatchAlts (stx : Syntax) : Array MatchAltView := do
   let matchAlts  := stx[4]
   let firstVBar  := matchAlts[0]
-  let ref        := firstVBar
-  let result     := #[]
+  let mut ref    := firstVBar
+  let mut result := #[]
   for arg in matchAlts[1].getArgs do
-    if ref.isNone then ref := arg -- The first vertical bar is optional
+    if ref.isNone then
+      ref := arg -- The first vertical bar is optional
     if arg.getKind == `Lean.Parser.Term.matchAlt then
       result := result.push (mkMatchAltView ref arg)
     else
@@ -220,7 +221,7 @@ private def throwCtorExpected {α} : M α :=
 
 private def getNumExplicitCtorParams (ctorVal : ConstructorVal) : TermElabM Nat :=
   forallBoundedTelescope ctorVal.type ctorVal.nparams fun ps _ => do
-    let result := 0
+    let mut result := 0
     for p in ps do
       let localDecl ← getLocalDecl p.fvarId!
       if localDecl.binderInfo.isExplicit then
@@ -463,7 +464,7 @@ partial def collect : Syntax → M Syntax
       let id := stx[0]
       processVar id
       let pat := stx[2]
-      pat ← collect pat
+      let pat ← collect pat
       `(namedPattern $id $pat)
     else if k == `Lean.Parser.Term.inaccessible then
       pure stx
@@ -547,8 +548,8 @@ private partial def withPatternVars {α} (pVars : Array PatternVar) (k : Array P
   loop 0 #[]
 
 private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : TermElabM (Array Expr × Expr) := do
-  let patterns  := #[]
-  let matchType := matchType
+  let mut patterns  := #[]
+  let mut matchType := matchType
   for patternStx in patternStxs do
     matchType ← whnf matchType
     match matchType with
@@ -560,7 +561,7 @@ private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : TermE
   pure (patterns, matchType)
 
 def finalizePatternDecls (patternVarDecls : Array PatternVarDecl) : TermElabM (Array LocalDecl) := do
-  let decls := #[]
+  let mut decls := #[]
   for pdecl in patternVarDecls do
     match pdecl with
     | PatternVarDecl.localVar fvarId =>
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 1ecb0e80a9..b8f401223f 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -88,7 +88,7 @@ private def elabFunType (ref : Syntax) (xs : Array Expr) (view : DefView) : Term
     mkForallFVars xs type
 
 private def elabHeaders (views : Array DefView) : TermElabM (Array DefViewElabHeader) := do
-  let headers := #[]
+  let mut headers := #[]
   for view in views do
     let newHeader ← withRef view.ref do
       let ⟨shortDeclName, declName, levelNames⟩ ← expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
@@ -262,16 +262,16 @@ Note that `g` is not a free variable at `(let g : B := ?m₂; body)`. We recover
 -/
 private def mkInitialUsedFVarsMap (mctx : MetavarContext) (sectionVars : Array Expr) (mainFVarIds : Array FVarId) (letRecsToLift : List LetRecToLift)
     : UsedFVarsMap := do
-  let sectionVarSet := {}
+  let mut sectionVarSet := {}
   for var in sectionVars do
     sectionVarSet := sectionVarSet.insert var.fvarId!
-  let usedFVarMap := {}
+  let mut usedFVarMap := {}
   for mainFVarId in mainFVarIds do
     usedFVarMap := usedFVarMap.insert mainFVarId sectionVarSet
   for toLift in letRecsToLift do
     let state := Lean.collectFVars {} toLift.val
     let state := Lean.collectFVars state toLift.type
-    let set   := state.fvarSet
+    let mut set := state.fvarSet
     /- toLift.val may contain metavariables that are placeholders for nested let-recs. We should collect the fvarId
        for the associated let-rec because we need this information to compute the fixpoint later. -/
     let mvarIds := (toLift.val.collectMVars {}).result
@@ -363,7 +363,7 @@ private def mkFreeVarMap
   let usedFVarsMap  := mkInitialUsedFVarsMap mctx sectionVars mainFVarIds letRecsToLift
   let letRecFVarIds := letRecsToLift.map fun toLift => toLift.fvarId
   let usedFVarsMap  := FixPoint.run letRecFVarIds usedFVarsMap
-  let freeVarMap := {}
+  let mut freeVarMap := {}
   for toLift in letRecsToLift do
     let lctx       := toLift.lctx
     let fvarIdsSet := (usedFVarsMap.find? toLift.fvarId).get!
diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
index f32aeef55c..77de270d4b 100644
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -46,7 +46,7 @@ def levelMVarToParamPreDecls (preDefs : Array PreDefinition) : TermElabM (Array
   (levelMVarToParamPreDeclsAux preDefs).run' 1
 
 private def getLevelParamsPreDecls (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (List Name) := do
-  let s : CollectLevelParams.State := {}
+  let mut s : CollectLevelParams.State := {}
   for preDef in preDefs do
     s := collectLevelParams s preDef.type
     s := collectLevelParams s preDef.value
diff --git a/src/Lean/Elab/PreDefinition/Structural.lean b/src/Lean/Elab/PreDefinition/Structural.lean
index 7a6c59a018..7dbfff3c9e 100644
--- a/src/Lean/Elab/PreDefinition/Structural.lean
+++ b/src/Lean/Elab/PreDefinition/Structural.lean
@@ -36,7 +36,7 @@ structure RecArgInfo :=
   (reflexive   : Bool)        -- true if we are recursing over a reflexive inductive datatype
 
 private def getIndexMinPos (xs : Array Expr) (indices : Array Expr) : Nat := do
-  let minPos := xs.size
+  let mut minPos := xs.size
   for index in indices do
     match xs.indexOf? index with
     | some pos => if pos.val < minPos then minPos := pos.val
@@ -232,7 +232,7 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
             -- Recall that the fixed parameters are not in the scope of the `brecOn`. So, we skip them.
             let argsNonFixed := args.extract numFixed args.size
             -- The function `f` does not explicitly take `recArg` and its indices as arguments. So, we skip them too.
-            let fArgs := #[]
+            let mut fArgs := #[]
             for i in [:argsNonFixed.size] do
               if recArgInfo.pos != i && !recArgInfo.indicesPos.contains i then
                 let arg := argsNonFixed[i]
@@ -281,7 +281,7 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
              This may generate weird error messages, when it doesn't work.
           -/
           let matcherApp ← mapError (matcherApp.addArg below) (fun msg => "failed to add `below` argument to 'matcher' application" ++ indentD msg)
-          let discrs := matcherApp.discrs
+          let mut discrs := matcherApp.discrs
           for i in [:discrs.size] do
             let discr ← processApp discrs[i]
             trace[Elab.definition.structural]! "new discr [{i}]: {discr}"
@@ -304,7 +304,7 @@ private def mkBRecOn (recFnName : Name) (recArgInfo : RecArgInfo) (value : Expr)
   let major := recArgInfo.ys[recArgInfo.pos]
   let otherArgs := recArgInfo.ys.filter fun y => y != major && !recArgInfo.indIndices.contains y
   let motive ← mkForallFVars otherArgs type
-  let brecOnUniv ← getLevel motive
+  let mut brecOnUniv ← getLevel motive
   trace[Elab.definition.structural]! "brecOn univ: {brecOnUniv}"
   let useBInductionOn := recArgInfo.reflexive && brecOnUniv == levelZero
   if recArgInfo.reflexive && brecOnUniv != levelZero then
diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index 3d2528eb41..72a82c060e 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -15,7 +15,7 @@ private def lparamsToMessageData (lparams : List Name) : MessageData :=
   match lparams with
   | []    => ""
   | u::us => do
-    let m : MessageData := ".{" ++ u
+    let mut m : MessageData := ".{" ++ u
     for u in us do
       m := m ++ ", " ++ u
     return m ++ "}"
@@ -42,8 +42,8 @@ private def printQuot (kind : QuotKind) (id : Name) (lparams : List Name) (type
 
 private def printInduct (id : Name) (lparams : List Name) (nparams : Nat) (nindices : Nat) (type : Expr)
     (ctors : List Name) (isUnsafe : Bool) : CommandElabM Unit := do
-  let m ← mkHeader "inductive" id lparams type isUnsafe
-  let m := m ++ Format.line ++ "constructors:"
+  let mut m ← mkHeader "inductive" id lparams type isUnsafe
+  m := m ++ Format.line ++ "constructors:"
   for ctor in ctors do
     let cinfo ← getConstInfo ctor
     m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index fd847b5837..a8f2a7d7d8 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -529,7 +529,7 @@ private partial def elabStruct (s : Struct) (expectedType? : Option Expr) : Term
           -- if all fields of `s` are marked as `default`, then try to synthesize instance
           match (← trySynthStructInstance? s d) with
           | some val => cont val { field with val := FieldVal.term (mkHole field.ref) }
-          | none     => do let (val, sNew) ← elabStruct s (some d); val ← ensureHasType d val; cont val { field with val := FieldVal.nested sNew }
+          | none     => do let (val, sNew) ← elabStruct s (some d); let val ← ensureHasType d val; cont val { field with val := FieldVal.nested sNew }
         | FieldVal.default  => do let val ← withRef field.ref $ mkFreshExprMVar (some d); cont (markDefaultMissing val) field
       | _ => withRef field.ref $ throwFailedToElabField fieldName s.structName msg!"unexpected constructor type{indentExpr type}"
     | _ => throwErrorAt field.ref "unexpected unexpanded structure field"
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index af7d228838..caf79afa37 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -25,7 +25,7 @@ private def mkParserSeq (ds : Array Syntax) : TermElabM Syntax := do
   else if ds.size == 1 then
     pure ds[0]
   else
-    let r := ds[0]
+    let mut r := ds[0]
     for d in ds[1:ds.size] do
       r ← `(ParserDescr.andthen $r $d)
     return r
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index f7665bcfde..56089fdc84 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -253,13 +253,13 @@ def «try» {α} (tactic : TacticM α) : TacticM Bool := do
   If there is only one new untagged goal, then we just use `parentTag` -/
 def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVarId) : TacticM Unit := do
   let mctx ← getMCtx
-  let numAnonymous := 0
+  let mut numAnonymous := 0
   for g in newGoals do
     if mctx.isAnonymousMVar g then
       numAnonymous := numAnonymous + 1
   modifyMCtx fun mctx => do
-    let mctx := mctx
-    let idx  := 1
+    let mut mctx := mctx
+    let mut idx  := 1
     for g in newGoals do
       if mctx.isAnonymousMVar g then
         if numAnonymous == 1 then
diff --git a/src/Lean/Elab/Tactic/Generalize.lean b/src/Lean/Elab/Tactic/Generalize.lean
index ed4484587a..aed41f3c65 100644
--- a/src/Lean/Elab/Tactic/Generalize.lean
+++ b/src/Lean/Elab/Tactic/Generalize.lean
@@ -27,7 +27,7 @@ private def evalGeneralizeFinalize (mvarId : MVarId) (e : Expr) (target : Expr)
   let val    := mkApp2 mvar' e rfl
   assignExprMVar mvarId val
   let mvarId' := mvar'.mvarId!
-  (_, mvarId') ← Meta.introNP mvarId' 2
+  let (_, mvarId') ← Meta.introNP mvarId' 2
   pure [mvarId']
 
 private def evalGeneralizeWithEq (h : Name) (e : Expr) (x : Name) : TacticM Unit :=
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 2b40c845e9..20cfa91808 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -153,10 +153,10 @@ private def checkAltNames (alts : Array (Name × MVarId)) (altsSyntax : Array Sy
 def evalAlts (elimInfo : ElimInfo) (alts : Array (Name × MVarId)) (altsSyntax : Array Syntax)
     (numEqs : Nat := 0) (numGeneralized : Nat := 0) (toClear : Array FVarId := #[]) : TacticM Unit := do
   checkAltNames alts altsSyntax
-  let usedWildcard := false
-  let hasAlts      := altsSyntax.size > 0
-  let subgoals     := #[] -- when alternatives are not provided, we accumulate subgoals here
-  let altsSyntax   := altsSyntax
+  let mut usedWildcard := false
+  let hasAlts := altsSyntax.size > 0
+  let mut subgoals := #[] -- when alternatives are not provided, we accumulate subgoals here
+  let mut altsSyntax := altsSyntax
   for (altName, altMVarId) in alts do
     let numFields ← getAltNumFields elimInfo altName
     let altStx? ←
@@ -173,7 +173,7 @@ def evalAlts (elimInfo : ElimInfo) (alts : Array (Name × MVarId)) (altsSyntax :
           pure none
     match altStx? with
     | none =>
-      let (_, altMVarId) ← introN altMVarId numFields
+      let mut (_, altMVarId) ← introN altMVarId numFields
       match (← Cases.unifyEqs numEqs altMVarId {}) with
       | none   => pure () -- alternative is not reachable
       | some (altMVarId, _) =>
@@ -190,7 +190,7 @@ def evalAlts (elimInfo : ElimInfo) (alts : Array (Name × MVarId)) (altsSyntax :
       subgoals ← withRef altStx do
         let altRhs := getAltRHS altStx
         let altVarNames := getAltVarNames altStx
-        let (_, altMVarId) ← introN altMVarId numFields altVarNames.toList
+        let mut (_, altMVarId) ← introN altMVarId numFields altVarNames.toList
         match (← Cases.unifyEqs numEqs altMVarId {}) with
         | none   => throwError! "alternative '{altName}' is not needed"
         | some (altMVarId, _) =>
@@ -240,7 +240,7 @@ private def getAlts (withAlts : Syntax) : Array Syntax :=
   We may have at most one `| _ => ...` (wildcard alternative), and it must not set variable names.
   The idea is to make sure users do not write unstructured tactics. -/
 private def checkAlts (withAlts : Syntax) : TacticM Unit := do
-  let found := false
+  let mut found := false
   for alt in getAlts withAlts do
     let n := getAltName alt
     if n == `_ then
@@ -318,11 +318,11 @@ private def getRecInfoDefault (major : Expr) (withAlts : Syntax) (allowMissingAl
     let ctorNames := indVal.ctors
     let alts      := getAlts withAlts
     checkAltCtorNames alts ctorNames
-    let altVars := #[]
-    let altRHSs := #[]
+    let mut altVars := #[]
+    let mut altRHSs := #[]
     -- This code can be simplified if we decide to keep `checkAlts`
-    let remainingAlts := alts
-    let prevAnonymousAlt? := none
+    let mut remainingAlts := alts
+    let mut prevAnonymousAlt? := none
     for ctorName in ctorNames do
       match remainingAlts.findIdx? (fun alt => (getAltName alt).isSuffixOf ctorName) with
       | some idx =>
@@ -377,10 +377,10 @@ private def getRecInfo (stx : Syntax) (major : Expr) : TacticM RecInfo := withRe
     else
       let alts := getAlts withAlts
       let paramNames ← liftMetaMAtMain fun _ => getParamNames recInfo.recursorName
-      let altVars           := #[]
-      let altRHSs           := #[]
-      let remainingAlts     := alts
-      let prevAnonymousAlt? := none
+      let mut altVars           := #[]
+      let mut altRHSs           := #[]
+      let mut remainingAlts     := alts
+      let mut prevAnonymousAlt? := none
       for i in [:paramNames.size] do
         if recInfo.isMinor i then
           let paramName := paramNames[i]
@@ -413,12 +413,12 @@ private def processResult (altRHSs : Array Syntax) (result : Array Meta.Inductio
   else
     unless altRHSs.size == result.size do
       throwError! "mistmatch on the number of subgoals produced ({result.size}) and alternatives provided ({altRHSs.size})"
-    let gs := #[]
+    let mut gs := #[]
     for i in [:result.size] do
       let subgoal := result[i]
       let rhs     := altRHSs[i]
       let ref     := rhs
-      let mvarId  := subgoal.mvarId
+      let mut mvarId := subgoal.mvarId
       if numToIntro > 0 then
         (_, mvarId) ← introNP mvarId numToIntro
       gs ← evalAltRhs mvarId rhs gs
diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean
index 29ff01f6b5..8cef19f4a5 100644
--- a/src/Lean/Elab/Tactic/Rewrite.lean
+++ b/src/Lean/Elab/Tactic/Rewrite.lean
@@ -42,7 +42,7 @@ def rewriteLocalDecl (stx : Syntax) (symm : Bool) (userName : Name) : TacticM Un
 def rewriteAll (stx : Syntax) (symm : Bool) : TacticM Unit := do
   let worked ← «try» $ rewriteTarget stx symm
   withMainMVarContext do
-    let worked := worked
+    let mut worked := worked
     -- We must traverse backwards because `replaceLocalDecl` uses the revert/intro idiom
     for fvarId in (← getLCtx).getFVarIds.reverse do
       worked := worked || (← «try» $ rewriteLocalDeclFVarId stx symm fvarId)
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 1a828df0d7..ffa3ebcb2d 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -499,7 +499,7 @@ private partial def getEntriesFor (mod : ModuleData) (extId : Name) (i : Nat) :
     #[]
 
 private def setImportedEntries (env : Environment) (mods : Array ModuleData) : IO Environment := do
-  let env := env
+  let mut env := env
   let pExtDescrs ← persistentEnvExtensionsRef.get
   for mod in mods do
     for extDescr in pExtDescrs do
@@ -508,7 +508,7 @@ private def setImportedEntries (env : Environment) (mods : Array ModuleData) : I
   return env
 
 private def finalizePersistentExtensions (env : Environment) (opts : Options) : IO Environment := do
-  let env := env
+  let mut env := env
   let pExtDescrs ← persistentEnvExtensionsRef.get
   for extDescr in pExtDescrs do
     let s := extDescr.toEnvExtension.getState env
@@ -519,9 +519,9 @@ private def finalizePersistentExtensions (env : Environment) (opts : Options) :
 @[export lean_import_modules]
 def importModules (imports : List Import) (opts : Options) (trustLevel : UInt32 := 0) : IO Environment := profileitIO "import" ⟨0, 0⟩ do
   let (moduleNames, mods, regions) ← importModulesAux imports ({}, #[], #[])
-  let modIdx : Nat := 0
-  let const2ModIdx : HashMap Name ModuleIdx := {}
-  let constants : ConstMap := SMap.empty
+  let mut modIdx : Nat := 0
+  let mut const2ModIdx : HashMap Name ModuleIdx := {}
+  let mut constants : ConstMap := SMap.empty
   for mod in mods do
     for cinfo in mod.constants do
       const2ModIdx := const2ModIdx.insert cinfo.name modIdx
diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean
index f3b16a656d..31df038786 100644
--- a/src/Lean/Meta/AbstractNestedProofs.lean
+++ b/src/Lean/Meta/AbstractNestedProofs.lean
@@ -36,7 +36,7 @@ partial def visit (e : Expr) : M Expr := do
   else
     let visitBinders (xs : Array Expr) (k : M Expr) : M Expr := do
       let localInstances ← getLocalInstances
-      let lctx ← getLCtx
+      let mut lctx ← getLCtx
       for x in xs do
         let xFVarId := x.fvarId!
         let localDecl ← getLocalDecl xFVarId
diff --git a/src/Lean/Meta/FunInfo.lean b/src/Lean/Meta/FunInfo.lean
index 247b856658..1380579944 100644
--- a/src/Lean/Meta/FunInfo.lean
+++ b/src/Lean/Meta/FunInfo.lean
@@ -55,7 +55,7 @@ private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
     let fnType ← inferType fn
     withTransparency TransparencyMode.default $
       forallBoundedTelescope fnType maxArgs? fun fvars type => do
-        let pinfo := #[]
+        let mut pinfo := #[]
         for i in [:fvars.size] do
           let fvar := fvars[i]
           let decl ← getFVarLocalDecl fvar
diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean
index 73febfcd4d..2e0632a459 100644
--- a/src/Lean/Meta/InferType.lean
+++ b/src/Lean/Meta/InferType.lean
@@ -12,8 +12,8 @@ def throwFunctionExpected {α} (f : Expr) : MetaM α :=
   throwError! "function expected{indentExpr f}"
 
 private def inferAppType (f : Expr) (args : Array Expr) : MetaM Expr := do
-  let fType ← inferType f
-  let j := 0
+  let mut fType ← inferType f
+  let mut j := 0
   for i in [:args.size] do
     match fType with
     | Expr.forallE _ _ b _ => fType := b
@@ -43,7 +43,7 @@ private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Exp
     let structParams := structType.getAppArgs
     if n != structParams.size then failed ()
     else do
-      let ctorType ← inferAppType (mkConst ctorVal.name structLvls) structParams
+      let mut ctorType ← inferAppType (mkConst ctorVal.name structLvls) structParams
       for i in [:idx] do
         ctorType ← whnf ctorType
         match ctorType with
@@ -210,7 +210,7 @@ private def isPropImp (e : Expr) : MetaM Bool := do
     let type ← inferType e
     let type ← whnfD type
     match type with
-    | Expr.sort u _ => do u ← instantiateLevelMVars u; pure $ isAlwaysZero u
+    | Expr.sort u _ => return isAlwaysZero (← instantiateLevelMVars u)
     | _             => pure false
 
 def isProp (e : Expr) : m Bool :=
diff --git a/src/Lean/Meta/LevelDefEq.lean b/src/Lean/Meta/LevelDefEq.lean
index 3431d0e099..672ceeb416 100644
--- a/src/Lean/Meta/LevelDefEq.lean
+++ b/src/Lean/Meta/LevelDefEq.lean
@@ -224,7 +224,7 @@ private def restore (env : Environment) (mctx : MetavarContext) (postponed : Per
     throw ex
 
 private def postponedToMessageData (ps : PersistentArray PostponedEntry) : MessageData := do
-  let r := MessageData.nil
+  let mut r := MessageData.nil
   for p in ps do
     r := msg!"{r}\n{p.lhs} =?= {p.rhs}"
   pure r
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index c750af5eea..3680baedf9 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -678,7 +678,7 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
           | Pattern.var _ :: _         => true
           | _                          => false
         let newAlts := newAlts.map fun alt => alt.applyFVarSubst subst
-        newAlts ← newAlts.mapM fun alt => match alt.patterns with
+        let newAlts ← newAlts.mapM fun alt => match alt.patterns with
           | Pattern.arrayLit _ pats :: ps => pure { alt with patterns := pats ++ ps }
           | Pattern.var fvarId :: ps      => do let α ← getArrayArgType x; expandVarIntoArrayLit { alt with patterns := ps } fvarId α size
           | _  => unreachable!
diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean
index df8c45d33d..426d322cfe 100644
--- a/src/Lean/Meta/RecursorInfo.lean
+++ b/src/Lean/Meta/RecursorInfo.lean
@@ -145,7 +145,7 @@ private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs :
     | none          => throwError! "ill-formed recursor '{declName}'"
 
 private def getParamsPos (declName : Name) (xs : Array Expr) (numParams : Nat) (Iargs : Array Expr) : MetaM (List (Option Nat)) := do
-  let paramsPos := #[]
+  let mut paramsPos := #[]
   for i in [:numParams] do
     let x := xs[i]
     match (← Iargs.findIdxM? fun Iarg => isDefEq Iarg x) with
@@ -159,7 +159,7 @@ private def getParamsPos (declName : Name) (xs : Array Expr) (numParams : Nat) (
   pure paramsPos.toList
 
 private def getIndicesPos (declName : Name) (xs : Array Expr) (majorPos numIndices : Nat) (Iargs : Array Expr) : MetaM (List Nat) := do
-  let indicesPos := #[]
+  let mut indicesPos := #[]
   for i in [:numIndices] do
     let i := majorPos - numIndices + i
     let x := xs[i]
@@ -177,7 +177,7 @@ private def getMotiveLevel (declName : Name) (motiveResultType : Expr) : MetaM L
 
 private def getUnivLevelPos (declName : Name) (lparams : List Name) (motiveLvl : Level) (Ilevels : List Level) : MetaM (List RecursorUnivLevelPos) := do
   let Ilevels := Ilevels.toArray
-  let univLevelPos := #[]
+  let mut univLevelPos := #[]
   for p in lparams do
     if motiveLvl == mkLevelParam p then
       univLevelPos := univLevelPos.push RecursorUnivLevelPos.motive
@@ -189,8 +189,8 @@ private def getUnivLevelPos (declName : Name) (lparams : List Name) (motiveLvl :
   pure univLevelPos.toList
 
 private def getProduceMotiveAndRecursive (xs : Array Expr) (numParams numIndices majorPos : Nat) (motive : Expr) : MetaM (List Bool × Bool) := do
-  let produceMotive := #[]
-  let recursor      := false
+  let mut produceMotive := #[]
+  let mut recursor      := false
   for i in [:xs.size] do
     if i < numParams + 1 then
       continue --skip parameters and motive
diff --git a/src/Lean/Meta/Reduce.lean b/src/Lean/Meta/Reduce.lean
index 37b2ef6847..e80518b618 100644
--- a/src/Lean/Meta/Reduce.lean
+++ b/src/Lean/Meta/Reduce.lean
@@ -21,7 +21,7 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Meta
         let f     := e.getAppFn
         let nargs := e.getAppNumArgs
         let finfo ← getFunInfoNArgs f nargs
-        let args  := e.getAppArgs
+        let mut args  := e.getAppArgs
         for i in [:args.size] do
           if i < finfo.paramInfo.size then
             let info := finfo.paramInfo[i]
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 9d23d3689f..b9f1748ccb 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -485,7 +485,7 @@ private def preprocess (type : Expr) : MetaM Expr :=
     mkForallFVars xs type
 
 private def preprocessLevels (us : List Level) : MetaM (List Level) := do
-  let r := []
+  let mut r := []
   for u in us do
     let u ← instantiateLevelMVars u
     if u.hasMVar then
diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean
index bed50ae5de..3a037737c9 100644
--- a/src/Lean/Meta/Tactic/Apply.lean
+++ b/src/Lean/Meta/Tactic/Apply.lean
@@ -79,7 +79,7 @@ def apply (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) :=
     checkNotAssigned mvarId `apply
     let targetType ← getMVarType mvarId
     let eType      ← inferType e
-    let (numArgs, hasMVarHead) ← getExpectedNumArgsAux eType
+    let mut (numArgs, hasMVarHead) ← getExpectedNumArgsAux eType
     if hasMVarHead then
       let targetTypeNumArgs ← getExpectedNumArgs targetType
       numArgs := numArgs - targetTypeNumArgs
diff --git a/src/Lean/Meta/Tactic/ElimInfo.lean b/src/Lean/Meta/Tactic/ElimInfo.lean
index c2dea621f3..0f13e422ab 100644
--- a/src/Lean/Meta/Tactic/ElimInfo.lean
+++ b/src/Lean/Meta/Tactic/ElimInfo.lean
@@ -35,7 +35,7 @@ def getElimInfo (declName : Name) : MetaM ElimInfo := do
       match xs.indexOf? target with
       | none => throwError! "unexpected eliminator type{indentExpr declInfo.type}"
       | some targetPos => pure targetPos.val
-    let altsInfo := #[]
+    let mut altsInfo := #[]
     for i in [:xs.size] do
       let x := xs[i]
       if x != motive && !targets.contains x then
diff --git a/src/Lean/Meta/Tactic/Induction.lean b/src/Lean/Meta/Tactic/Induction.lean
index ea7c50d9bf..d079a16b7c 100644
--- a/src/Lean/Meta/Tactic/Induction.lean
+++ b/src/Lean/Meta/Tactic/Induction.lean
@@ -158,8 +158,8 @@ def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (gi
       let (majorFVarId', mvarId) ← intro1P mvarId
       -- Create FVarSubst with indices
       let baseSubst := do
-        let subst : FVarSubst := {}
-        let i := 0
+        let mut subst : FVarSubst := {}
+        let mut i := 0
         for index in indices do
           subst := subst.insert index.fvarId! (mkFVar indices'[i])
           i     := i + 1
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 52972d0459..858a985721 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -87,7 +87,7 @@ private def reduceRec {α} (recVal : RecursorVal) (recLvls : List Level) (recArg
   let majorIdx := recVal.getMajorIdx
   if h : majorIdx < recArgs.size then do
     let major := recArgs.get ⟨majorIdx, h⟩
-    let major ← whnf major
+    let mut major ← whnf major
     if recVal.k then
       let newMajor ← toCtorWhenK recVal major
       major := newMajor.getD major
@@ -121,7 +121,7 @@ private def reduceRec {α} (recVal : RecursorVal) (recLvls : List Level) (recArg
     let majorIdx := recVal.getMajorIdx
     if h : majorIdx < recArgs.size then do
       let major := recArgs.get ⟨majorIdx, h⟩
-      major ← whnf major
+      let major ← whnf major
       isStuck? major
     else
       pure none
@@ -135,7 +135,7 @@ private def reduceQuotRec {α} (recVal  : QuotVal) (recLvls : List Level) (recAr
   let process (majorPos argPos : Nat) : MetaM α :=
     if h : majorPos < recArgs.size then do
       let major := recArgs.get ⟨majorPos, h⟩
-      major ← whnf major
+      let major ← whnf major
       match major with
       | Expr.app (Expr.app (Expr.app (Expr.const majorFn _ _) _ _) _ _) majorArg _ => do
         let some (ConstantInfo.quotInfo { kind := QuotKind.ctor, .. }) ← getConstNoEx? majorFn | failK ()
@@ -156,7 +156,7 @@ private def reduceQuotRec {α} (recVal  : QuotVal) (recLvls : List Level) (recAr
   let process? (majorPos : Nat) : MetaM (Option MVarId) :=
     if h : majorPos < recArgs.size then do
       let major := recArgs.get ⟨majorPos, h⟩
-      major ← whnf major
+      let major ← whnf major
       isStuck? major
     else
       pure none
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 2f5104b803..3b2d13cb0e 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -719,7 +719,7 @@ instance : MonadHashMapCacheAdapter Expr Expr M := {
 
 /-- Return the local declaration of the free variable `x` in `xs` with the smallest index -/
 private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr) : LocalDecl := do
-  let d : LocalDecl := lctx.getFVar! xs[0]
+  let mut d : LocalDecl := lctx.getFVar! xs[0]
   for i in [1:xs.size] do
     let curr := lctx.getFVar! xs[i]
     if curr.index < d.index then
diff --git a/src/Lean/Parser/Transform.lean b/src/Lean/Parser/Transform.lean
index bbf13377e7..ac07659474 100644
--- a/src/Lean/Parser/Transform.lean
+++ b/src/Lean/Parser/Transform.lean
@@ -14,7 +14,7 @@ def manyToSepBy (stx : Syntax) (sepTk : String) : Syntax := do
     if args.size == 0 then
       stx
     else
-      let argsNew := #[args[0]]
+      let mut argsNew := #[args[0]]
       for i in [1:args.size] do
         let arg  := args[i]
         let prev := argsNew.back
diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index 51b287ca2c..9635809846 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -50,8 +50,8 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do
     let mkCall (p : Name) := do
       let ty ← inferType (mkConst p)
       forallTelescope ty fun params _ => do
-        let p    := mkConst p
-        let args := e.getAppArgs
+        let mut p := mkConst p
+        let args  := e.getAppArgs
         for i in [:Nat.min params.size args.size] do
           let param := params[i]
           let arg   := args[i]
diff --git a/src/Std/Data/PersistentArray.lean b/src/Std/Data/PersistentArray.lean
index 88acbefefc..17a6b3c770 100644
--- a/src/Std/Data/PersistentArray.lean
+++ b/src/Std/Data/PersistentArray.lean
@@ -210,7 +210,7 @@ variable {β : Type v}
 @[specialize]
 partial def forInAux {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] [inh : Inhabited β]
     (f : α → β → m (ForInStep β)) (n : PersistentArrayNode α) (b : β) : m (ForInStep β) := do
-  let b := b
+  let mut b := b
   match n with
   | leaf vs =>
     for v in vs do
@@ -229,6 +229,7 @@ partial def forInAux {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
   match (← forInAux (inh := ⟨init⟩) f t.root init) with
   | ForInStep.done b  => pure b
   | ForInStep.yield b =>
+    let mut b := b
     for v in t.tail do
       match (← f v b) with
       | ForInStep.done b => return b