From 5024c15a7a5e79790071bc30920ed16bf64f443d Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 7 Jul 2022 10:55:04 +0200
Subject: [PATCH] feat: add getConstInfoDefn

---
 src/Lean/MonadEnv.lean | 5 +++++
 1 file changed, 5 insertions(+)

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