diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index 7dffffae44..b5f1ae37f3 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -268,6 +268,12 @@ do mctx ← getMCtx;
    | some d => pure $ d.synthetic
    | _      => throwEx $ Exception.unknownExprMVar mvarId
 
+def isReadOnlyExprMVar (mvarId : Name) : MetaM Bool :=
+do mctx ← getMCtx;
+   match mctx.findDecl mvarId with
+   | some d => pure $ d.depth != mctx.depth
+   | _      => throwEx $ Exception.unknownExprMVar mvarId
+
 def isReadOnlyOrSyntheticExprMVar (mvarId : Name) : MetaM Bool :=
 do mctx ← getMCtx;
    match mctx.findDecl mvarId with