fix: don't generate code for decls with an implemented_by attribute

leanprover · Jan 17, 2025 · 7362de4 · 7362de4
1 parent e3fd954
commit 7362de4
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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