From 9feb4d8ab709affc567b353d9d84e92a730c1e2f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 9 Oct 2022 15:35:15 -0700 Subject: [PATCH] fix: do not generate code for `[extern]` functions --- 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 d972c72e74..ae3c3775c7 100644 --- a/src/Lean/Compiler/LCNF/Main.lean +++ b/src/Lean/Compiler/LCNF/Main.lean @@ -29,6 +29,7 @@ def shouldGenerateCode (declName : Name) : CoreM Bool := do let some info ← getDeclInfo? declName | return false unless info.hasValue do return false let env ← getEnv + if isExtern env declName then return false if hasMacroInlineAttribute env declName then return false if (← Meta.isMatcher declName) then return false if isCasesOnRecursor env declName then return false