From cbd022e4eb90ffdd6212f4ec2a07d8c58e3e3e50 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Aug 2022 10:32:45 -0700
Subject: [PATCH] refactor: `replaceFVarIdAtLocalDecl` =>
 `LocalDecl.replaceFVarId`

---
 src/Lean/Elab/MutualDef.lean   | 4 ++--
 src/Lean/LocalContext.lean     | 2 +-
 src/Lean/Meta/Closure.lean     | 2 +-
 src/Lean/Meta/Match/Basic.lean | 5 +++--
 4 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 9b6f91005c..2051f75906 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -528,8 +528,8 @@ private partial def mkClosureForAux (toProcess : Array FVarId) : StateRefT Closu
           newLetDecls   := s.newLetDecls.push <| LocalDecl.ldecl default fvarId userName type val false,
           /- We don't want to interleave let and lambda declarations in our closure. So, we expand any occurrences of fvarId
              at `newLocalDecls` and `localDecls` -/
-          newLocalDecls := s.newLocalDecls.map (replaceFVarIdAtLocalDecl fvarId val)
-          localDecls := s.localDecls.map (replaceFVarIdAtLocalDecl fvarId val)
+          newLocalDecls := s.newLocalDecls.map (·.replaceFVarId fvarId val)
+          localDecls := s.localDecls.map (·.replaceFVarId fvarId val)
         }
         mkClosureForAux (pushNewVars toProcess (collectFVars (collectFVars {} type) val))
 
diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index 4712e4de16..618115c4ef 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -423,7 +423,7 @@ export MonadLCtx (getLCtx)
 instance [MonadLift m n] [MonadLCtx m] : MonadLCtx n where
   getLCtx := liftM (getLCtx : m _)
 
-def replaceFVarIdAtLocalDecl (fvarId : FVarId) (e : Expr) (d : LocalDecl) : LocalDecl :=
+def LocalDecl.replaceFVarId (fvarId : FVarId) (e : Expr) (d : LocalDecl) : LocalDecl :=
   if d.fvarId == fvarId then d
   else match d with
     | .cdecl idx id n type bi => .cdecl idx id n (type.replaceFVarId fvarId e) bi
diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean
index 81ec6e2fc2..474ba06a1c 100644
--- a/src/Lean/Meta/Closure.lean
+++ b/src/Lean/Meta/Closure.lean
@@ -279,7 +279,7 @@ partial def process : ClosureM Unit := do
         modify fun s => { s with newLetDecls := s.newLetDecls.push <| LocalDecl.ldecl default newFVarId userName type val false }
         /- We don't want to interleave let and lambda declarations in our closure. So, we expand any occurrences of newFVarId
            at `newLocalDecls` -/
-        modify fun s => { s with newLocalDecls := s.newLocalDecls.map (replaceFVarIdAtLocalDecl newFVarId val) }
+        modify fun s => { s with newLocalDecls := s.newLocalDecls.map (·.replaceFVarId newFVarId val) }
         process
 
 @[inline] def mkBinding (isLambda : Bool) (decls : Array LocalDecl) (b : Expr) : Expr :=
diff --git a/src/Lean/Meta/Match/Basic.lean b/src/Lean/Meta/Match/Basic.lean
index 2cb8bd70c9..b7aa73012b 100644
--- a/src/Lean/Meta/Match/Basic.lean
+++ b/src/Lean/Meta/Match/Basic.lean
@@ -152,10 +152,11 @@ def applyFVarSubst (s : FVarSubst) (alt : Alt) : Alt :=
 def replaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) : Alt :=
   { alt with
     patterns  := alt.patterns.map fun p => p.replaceFVarId fvarId v,
+    rhs       := alt.rhs.replaceFVarId fvarId v
     fvarDecls :=
       let decls := alt.fvarDecls.filter fun d => d.fvarId != fvarId
-      decls.map $ replaceFVarIdAtLocalDecl fvarId v,
-    rhs       := alt.rhs.replaceFVarId fvarId v }
+      decls.map (·.replaceFVarId fvarId v)
+  }
 
 /--
   Similar to `checkAndReplaceFVarId`, but ensures type of `v` is definitionally equal to type of `fvarId`.