max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add getConstInfoDefn

Browse source
This commit is contained in:
Gabriel Ebner 2022-07-07 10:55:04 +02:00 • committed by Leonardo de Moura
parent 3776e3c925
commit 5024c15a7a
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/MonadEnv.lean
View file

@ -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