From 238c2b3d174eb91848a00caa2693eb504e530072 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 14 Nov 2019 09:52:36 -0800 Subject: [PATCH] chore: add helper method --- library/Init/Lean/Meta/Basic.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/library/Init/Lean/Meta/Basic.lean b/library/Init/Lean/Meta/Basic.lean index 88104bc685..791834bb94 100644 --- a/library/Init/Lean/Meta/Basic.lean +++ b/library/Init/Lean/Meta/Basic.lean @@ -124,6 +124,9 @@ instance MetaM.inhabited {α} : Inhabited (MetaM α) := @[inline] def getLCtx : MetaM LocalContext := do ctx ← read; pure ctx.lctx +@[inline] def getConfig : MetaM Config := +do ctx ← read; pure ctx.config + @[inline] def getMCtx : MetaM MetavarContext := do s ← get; pure s.mctx