From 3eabda1c4d31d864a2cb9eaaead00d9124052115 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 2 Dec 2019 12:48:34 -0800
Subject: [PATCH] feat: add `withMCtx`

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

diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index 5dda5df5a0..fb6186a5d4 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -726,6 +726,11 @@ do mvarDecl ← getMVarDecl mvarId;
      else
        resettingSynthInstanceCache x
 
+@[inline] def withMCtx {α} (mctx : MetavarContext) (x : MetaM α) : MetaM α :=
+do mctx' ← getMCtx;
+   modify $ fun s => { mctx := mctx, .. s };
+   finally x (modify $ fun s => { mctx := mctx', .. s })
+
 end Meta
 end Lean