fix: skip declarations that do not have a value

This commit is contained in:
Leonardo de Moura 2022-09-21 18:40:20 -07:00
parent 574c75081f
commit 05f0a6c423

View file

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