source
opaque Lean.exportAttr :
ParametricAttribute Name

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