diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean index 8d0b7df77b..1cac4951e3 100644 --- a/src/Lean/Compiler/LCNF/Main.lean +++ b/src/Lean/Compiler/LCNF/Main.lean @@ -33,6 +33,7 @@ def shouldGenerateCode (declName : Name) : CoreM Bool := do let some info ← getDeclInfo? declName | return false unless info.hasValue (allowOpaque := true) do return false if hasMacroInlineAttribute env declName then return false + if (getImplementedBy? env declName).isSome then return false if (← Meta.isMatcher declName) then return false if isCasesOnRecursor env declName then return false -- TODO: check if type class instance