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

fix: checkIsDefinition

Browse source 
For '[inline] partial' definitions in mutual blocks.
This commit is contained in:
Leonardo de Moura 2020-10-12 15:57:39 -07:00
parent c1f2635391
commit 07254fc71b
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Compiler/Util.lean
View file

@ -78,9 +78,10 @@ private def getDeclNamesForCodeGen : Declaration → List Name
def checkIsDefinition (env : Environment) (n : Name) : Except String Unit :=
match env.find? n with
| (some (ConstantInfo.defnInfo _)) => Except.ok ()
| none => Except.error "unknow declaration"
| _ => Except.error "declaration is not a definition"
| (some (ConstantInfo.defnInfo _)) => Except.ok ()
| (some (ConstantInfo.opaqueInfo _)) => Except.ok ()
| none => Except.error ("unknow declaration '" ++ toString n ++ "'")
| _ => Except.error ("declaration is not a definition '" ++ toString n ++ "'")
/--
We generate auxiliary unsafe definitions for regular recursive definitions.