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

fix: usesLeanAPI

Browse source
This commit is contained in:
Leonardo de Moura 2020-05-26 14:57:29 -07:00
parent 17b6957f6c
commit 862795e9e9
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Compiler/IR/EmitC.lean
View file

@ -142,7 +142,7 @@ match d with
| Decl.fdecl f xs t b => do
unless (xs.size == 2 || xs.size == 1) (throw "invalid main function, incorrect arity when generating code");
env ← getEnv;
let usesLeanAPI := usesModuleFrom env `Init.Lean;
let usesLeanAPI := usesModuleFrom env `Lean;
if usesLeanAPI then
emitLn "void lean_initialize();"
else