From 8b4cdcfddde9cbcdd0507601b2721aebf9f5e0fe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 22 May 2021 19:24:41 -0700 Subject: [PATCH] chore: fix mutable variable shadowing --- src/Lean/Elab/BuiltinNotation.lean | 8 ++++---- src/Lean/Elab/Inductive.lean | 6 +++--- src/Lean/Elab/Quotation.lean | 16 ++++++++-------- src/Lean/Elab/Tactic/Induction.lean | 12 ++++++------ src/Lean/Meta/FunInfo.lean | 2 +- src/Lean/Meta/WHNF.lean | 2 +- src/Lean/Parser/Basic.lean | 8 ++++---- src/Lean/Syntax.lean | 6 +++--- src/Std/Data/PersistentArray.lean | 6 +++--- 9 files changed, 33 insertions(+), 33 deletions(-) diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index 498c3b3a33..61dbb01f0b 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -292,10 +292,10 @@ where @[builtinTermElab stateRefT] def elabStateRefT : TermElab := fun stx _ => do let σ ← elabType stx[1] - 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)) + let mut mStx := stx[2] + if mStx.getKind == `Lean.Parser.Term.macroDollarArg then + mStx := mStx[1] + let m ← elabTerm mStx (← mkArrow (mkSort levelOne) (mkSort levelOne)) let ω ← mkFreshExprMVar (mkSort levelOne) let stWorld ← mkAppM `STWorld #[ω, m] discard <| mkInstMVar stWorld diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 8e402c3319..83699abf8f 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -469,14 +469,14 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) : let rs ← elabHeader views withInductiveLocalDecls rs fun params indFVars => do let numExplicitParams := params.size - let mut indTypes := #[] + let mut indTypesArray := #[] for i in [:views.size] do let indFVar := indFVars[i] let r := rs[i] let type ← mkForallFVars params r.type let ctors ← elabCtors indFVars indFVar params r - indTypes := indTypes.push { name := r.view.declName, type := type, ctors := ctors : InductiveType } - let indTypes := indTypes.toList + indTypesArray := indTypesArray.push { name := r.view.declName, type := type, ctors := ctors : InductiveType } + let indTypes := indTypesArray.toList Term.synthesizeSyntheticMVarsNoPostponing let u ← getResultingUniverse indTypes let inferLevel ← shouldInferResultUniverse u diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 9f78e7f43a..5678806277 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -448,23 +448,23 @@ private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : T for alt in alts do let mut alt := alt match alt with - | (covered f exh, alt) => + | (covered f exh, alt') => -- we can only factor out a common check if there are no undecided patterns in between; -- otherwise we would change the order of alternatives if undecidedAlts.isEmpty then - yesAlts ← yesAlts.push <$> f (alt.1.tail!, alt.2) + yesAlts ← yesAlts.push <$> f (alt'.1.tail!, alt'.2) if !exh then - nonExhaustiveAlts := nonExhaustiveAlts.push alt + nonExhaustiveAlts := nonExhaustiveAlts.push alt' else - (floatedLetDecls, alt) ← deduplicate floatedLetDecls alt + (floatedLetDecls, alt) ← deduplicate floatedLetDecls alt' undecidedAlts := undecidedAlts.push alt nonExhaustiveAlts := nonExhaustiveAlts.push alt - | (undecided, alt) => - (floatedLetDecls, alt) ← deduplicate floatedLetDecls alt + | (undecided, alt') => + (floatedLetDecls, alt) ← deduplicate floatedLetDecls alt' undecidedAlts := undecidedAlts.push alt nonExhaustiveAlts := nonExhaustiveAlts.push alt - | (uncovered, alt) => - nonExhaustiveAlts := nonExhaustiveAlts.push alt + | (uncovered, alt') => + nonExhaustiveAlts := nonExhaustiveAlts.push alt' let mut stx ← info.doMatch (yes := fun newDiscrs => do let mut yesAlts := yesAlts diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index fb51a3bb0e..2ca1c79143 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -208,8 +208,8 @@ where let mut (_, altMVarId) ← introN altMVarId numFields match (← Cases.unifyEqs numEqs altMVarId {}) with | none => pure () -- alternative is not reachable - | some (altMVarId, _) => - let (_, altMVarId) ← introNP altMVarId numGeneralized + | some (altMVarId', _) => + (_, altMVarId) ← introNP altMVarId' numGeneralized for fvarId in toClear do altMVarId ← tryClear altMVarId fvarId let altMVarIds ← applyPreTac altMVarId @@ -234,8 +234,8 @@ where let mut (_, altMVarId) ← introN altMVarId numFields altVarNames.toList (useNamesForExplicitOnly := !altHasExplicitModifier altStx) match (← Cases.unifyEqs numEqs altMVarId {}) with | none => unusedAlt - | some (altMVarId, _) => - let (_, altMVarId) ← introNP altMVarId numGeneralized + | some (altMVarId', _) => + (_, altMVarId) ← introNP altMVarId' numGeneralized for fvarId in toClear do altMVarId ← tryClear altMVarId fvarId let altMVarIds ← applyPreTac altMVarId @@ -243,8 +243,8 @@ where unusedAlt else let mut subgoals := subgoals - for altMVarId in altMVarIds do - subgoals ← evalAlt altMVarId altStx subgoals + for altMVarId' in altMVarIds do + subgoals ← evalAlt altMVarId' altStx subgoals pure (subgoals, usedWildcard || isWildcard) if usedWildcard then altsSyntax := altsSyntax.filter fun alt => getAltName alt != `_ diff --git a/src/Lean/Meta/FunInfo.lean b/src/Lean/Meta/FunInfo.lean index c7d17a569a..73fd7cf917 100644 --- a/src/Lean/Meta/FunInfo.lean +++ b/src/Lean/Meta/FunInfo.lean @@ -67,7 +67,7 @@ private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo := instImplicit := decl.binderInfo == BinderInfo.instImplicit } let resultDeps := collectDeps fvars type - let pinfo := updateHasFwdDeps pinfo resultDeps + pinfo := updateHasFwdDeps pinfo resultDeps pure { resultDeps := resultDeps, paramInfo := pinfo } def getFunInfo (fn : Expr) : MetaM FunInfo := diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 8dc78d2bc4..7a02c30814 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -95,7 +95,7 @@ private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (recArgs : A if recVal.k then let newMajor ← toCtorWhenK recVal major major := newMajor.getD major - let major := toCtorIfLit major + major := toCtorIfLit major match getRecRuleFor recVal major with | some rule => let majorArgs := major.getAppArgs diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index c149fcb012..26eb6471af 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -637,19 +637,19 @@ private partial def sepByFnAux (p : ParserFn) (sep : ParserFn) (allowTrailingSep if s.pos > pos then return s.mkNode nullKind iniSz else if pOpt then - let s := s.restore sz pos + s := s.restore sz pos return s.mkNode nullKind iniSz else -- append `Syntax.missing` to make clear that List is incomplete - let s := s.pushSyntax Syntax.missing + s := s.pushSyntax Syntax.missing return s.mkNode nullKind iniSz if s.stackSize > sz + 1 then s := s.mkNode nullKind sz let sz := s.stackSize let pos := s.pos - let s := sep c s + s := sep c s if s.hasError then - let s := s.restore sz pos + s := s.restore sz pos return s.mkNode nullKind iniSz if s.stackSize > sz + 1 then s := s.mkNode nullKind sz diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean index 5fca3f14d4..e62405c353 100644 --- a/src/Lean/Syntax.lean +++ b/src/Lean/Syntax.lean @@ -195,7 +195,7 @@ partial instance : ForIn m TopDown Syntax where for arg in args do match ← loop arg b with | ForInStep.yield b' => b := b' - | ForInStep.done b => return ForInStep.done b + | ForInStep.done b' => return ForInStep.done b' return ForInStep.yield b | ForInStep.done b => return ForInStep.done b match ← @loop stx init ⟨init⟩ with @@ -213,10 +213,10 @@ partial def reprint (stx : Syntax) : Option String := if kind == choiceKind then -- this visit the first arg twice, but that should hardly be a problem -- given that choice nodes are quite rare and small - let s ← reprint args[0] + let s0 ← reprint args[0] for arg in args[1:] do let s' ← reprint stx - guard (s == s') + guard (s0 == s') | _ => pure () return s where diff --git a/src/Std/Data/PersistentArray.lean b/src/Std/Data/PersistentArray.lean index d4a063e8a5..bbefc522fa 100644 --- a/src/Std/Data/PersistentArray.lean +++ b/src/Std/Data/PersistentArray.lean @@ -213,13 +213,13 @@ partial def forInAux {α : Type u} {β : Type v} {m : Type v → Type w} [Monad | leaf vs => for v in vs do match (← f v b) with - | r@(ForInStep.done b) => return r + | r@(ForInStep.done _) => return r | ForInStep.yield bNew => b := bNew return ForInStep.yield b | node cs => for c in cs do match (← forInAux f c b) with - | r@(ForInStep.done b) => return r + | r@(ForInStep.done _) => return r | ForInStep.yield bNew => b := bNew return ForInStep.yield b @@ -230,7 +230,7 @@ partial def forInAux {α : Type u} {β : Type v} {m : Type v → Type w} [Monad let mut b := b for v in t.tail do match (← f v b) with - | ForInStep.done b => return b + | ForInStep.done r => return r | ForInStep.yield bNew => b := bNew return b