From 05f0a6c4232d73c3944c7cc64d69cabf8a38f2f2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Sep 2022 18:40:20 -0700 Subject: [PATCH] fix: skip declarations that do not have a value --- src/Lean/Compiler/LCNF/Main.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean index 3567210231..cda179a42d 100644 --- a/src/Lean/Compiler/LCNF/Main.lean +++ b/src/Lean/Compiler/LCNF/Main.lean @@ -27,6 +27,7 @@ and `[specialize]` since they can be partially applied. -/ def shouldGenerateCode (declName : Name) : CoreM Bool := do if (← isCompIrrelevant |>.run') then return false + unless (← getConstInfo declName).hasValue do return false let env ← getEnv if hasMacroInlineAttribute env declName then return false if (← Meta.isMatcher declName) then return false