From 5e582823eca8edbb41fa458bbe9705be75a413e0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 28 Aug 2020 16:48:42 -0700
Subject: [PATCH] feat: add `MonadLCtx` and `MonadMCtx` helper classes

---
 src/Lean/LocalContext.lean   | 9 +++++++++
 src/Lean/MetavarContext.lean | 9 +++++++++
 2 files changed, 18 insertions(+)

diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index 752cc036b4..97f18415e3 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -348,4 +348,13 @@ Id.run $ lctx.anyM p
 Id.run $ lctx.allM p
 
 end LocalContext
+
+class MonadLCtx (m : Type → Type) :=
+(getLCtx : m LocalContext)
+
+export MonadLCtx (getLCtx)
+
+instance monadLCtxTrans (m n) [MonadLCtx m] [MonadLift m n] : MonadLCtx n :=
+{ getLCtx := liftM (getLCtx : m _) }
+
 end Lean
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 8516d4126d..8e79128086 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -1049,4 +1049,13 @@ let (e, s) := LevelMVarToParam.main e { paramNamePrefix := paramNamePrefix, alre
   expr          := e }
 
 end MetavarContext
+
+class MonadMCtx (m : Type → Type) :=
+(getMCtx : m MetavarContext)
+
+export MonadMCtx (getMCtx)
+
+instance monadMCtxTrans (m n) [MonadMCtx m] [MonadLift m n] : MonadMCtx n :=
+{ getMCtx := liftM (getMCtx : m _) }
+
 end Lean