Lean.Compiler.ExportAttr

Exports a function under the provided unmangled symbol name. This can be used to refer to Lean functions from other programming languages like C.

Example:

@[export lean_color_from_map]
def colorValue (properties : @& Std.HashMap String String) : UInt32 :=
  match properties["color"]? with
  | some "red" => 0xff0000
  | some "green" => 0x00ff00
  | some "blue" => 0x0000ff
  | _ => -1

C code:

#include <lean/lean.h>

uint32_t lean_color_from_map(b_lean_obj_arg properties);

void fill_rectangle_from_map(b_lean_obj_arg properties) {
    uint32_t color = lean_color_from_map(properties);
    // ...
}

The opposite of this is @[extern], which allows Lean functions to refer to functions from other programming languages.

source

@[export lean_get_export_name_for]

def Lean.getExportNameFor? (env : Environment) (n : Name) :

Option Name

Equations

Lean.getExportNameFor? env n = Lean.exportAttr.getParam? env n

Instances For

source

def Lean.isExport (env : Environment) (n : Name) :

Bool

Equations

Lean.isExport env n = ((Lean.getExportNameFor? env n).isSome || n == `main)

Instances For