diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean
index 8bb7b2be29..c604a22c30 100644
--- a/src/Lean/MonadEnv.lean
+++ b/src/Lean/MonadEnv.lean
@@ -97,6 +97,11 @@ def mkConstWithLevelParams [Monad m] [MonadEnv m] [MonadError m] (constName : Na
   let info ← getConstInfo constName
   return mkConst constName (info.levelParams.map mkLevelParam)
 
+def getConstInfoDefn [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m DefinitionVal := do
+  match (← getConstInfo constName) with
+  | ConstantInfo.defnInfo v => pure v
+  | _                       => throwError "'{mkConst constName}' is not a definition"
+
 def getConstInfoInduct [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m InductiveVal := do
   match (← getConstInfo constName) with
   | ConstantInfo.inductInfo v => pure v