From f2921993bbab29b41a3c5d571b299cb8e2b45562 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Aug 2022 11:21:55 -0700
Subject: [PATCH] feat: add `LocalContext.replaceFVarId`

---
 src/Lean/LocalContext.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index 618115c4ef..d3b708e831 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -429,4 +429,9 @@ def LocalDecl.replaceFVarId (fvarId : FVarId) (e : Expr) (d : LocalDecl) : Local
     | .cdecl idx id n type bi => .cdecl idx id n (type.replaceFVarId fvarId e) bi
     | .ldecl idx id n type val nonDep => .ldecl idx id n (type.replaceFVarId fvarId e) (val.replaceFVarId fvarId e) nonDep
 
+def LocalContext.replaceFVarId (fvarId : FVarId) (e : Expr) (lctx : LocalContext) : LocalContext :=
+  let lctx := lctx.erase fvarId
+  { fvarIdToDecl := lctx.fvarIdToDecl.map (·.replaceFVarId fvarId e)
+    decls := lctx.decls.map fun localDecl? => localDecl?.map (·.replaceFVarId fvarId e) }
+
 end Lean