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