From deacb03802deef62aa6f09ba3ffcddbe46709711 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 28 Nov 2019 05:34:12 -0800 Subject: [PATCH] feat: add `isReadOnlyExprMVar` --- src/Init/Lean/Meta/Basic.lean | 6 ++++++ 1 file changed, 6 insertions(+) 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