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