From e3771e3ad63aef8547cedeef549673baabe328ec Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Mon, 20 Jan 2025 18:06:41 -0800
Subject: [PATCH] fix: don't generate code for decls with an implemented_by
 attribute (#6680)

This PR makes the new code generator skip generating code for decls with
an implemented_by decl, just like the old code generator.
---
 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 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