max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: do not generate code for [extern] functions

Browse source
This commit is contained in:
Leonardo de Moura 2022-10-09 15:35:15 -07:00
parent 2e09ac16b1
commit 9feb4d8ab7
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Compiler/LCNF/Main.lean
View file

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