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

chore(library/init/lean/compiler): add export.lean

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-22 11:27:25 -07:00
parent 2408d6dd80
commit a8f8df1475
2 changed files with 13 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/init/lean/compiler/export.lean Normal file
View file

@ -0,0 +1,12 @@
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.lean.environment
namespace Lean
@[extern "lean_get_export_name_for"]
constant getExportNameFor (env : @& Environment) (n : @& Name) : Option Name := default _
end Lean

4
library/init/lean/compiler/ir/emitcpp.lean
View file

@ -7,6 +7,7 @@ prelude
import init.control.conditional
import init.lean.runtime
import init.lean.name_mangling
import init.lean.compiler.export
import init.lean.compiler.initattr
import init.lean.compiler.ir.compilerm
import init.lean.compiler.ir.emitutil
@ -15,9 +16,6 @@ import init.lean.compiler.ir.simpcase
namespace Lean
namespace IR
@[extern "lean_get_export_name_for"]
constant getExportNameFor (env : @& Environment) (n : @& Name) : Option Name := default _
namespace EmitCpp
def leanMainFn := "_lean_main"