Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/leanprover/lean4/llms.txt

Use this file to discover all available pages before exploring further.

Lean 4 ships with a well-defined Foreign Function Interface (FFI) that lets you call hand-written C or C++ code from Lean, and conversely expose Lean functions to C. The two directions use different attributes — @[extern] for importing C into Lean, and @[export] for exporting Lean to C — and both sides share the same set of C types defined in <lean/lean.h>.
The authoritative, fully detailed FFI specification lives in the Lean Language Reference. This page is a practical introduction that covers the most common patterns with runnable examples.

​
Importing C Functions into Lean

​
The @[extern] attribute

Mark an opaque Lean declaration with @[extern "c_function_name"] to tell the compiler that its implementation lives in an external C symbol. 
-- Lean side: declare the signature, implementation is in C
@[extern "my_add"]
opaque myAdd : UInt32 → UInt32 → UInt32

// C side: ffi_static.c
#include <stdint.h>

uint32_t my_add(uint32_t a, uint32_t b) {
  return a + b;
}
For scalar types (UInt8, UInt16, UInt32, UInt64, USize, Float, Float32), Lean passes the value directly as the corresponding C scalar — no boxing, no pointer. The Lean declaration above compiles to exactly uint32_t my_add(uint32_t, uint32_t).

​
Variant forms of @[extern]

The @[extern] attribute supports several forms documented in ExternAttr.lean: 
-- Simple: use the same name for all backends
@[extern "level_hash"]
opaque levelHash : Level → UInt64

-- Backend-specific names
@[extern cpp "lean::string_size" llvm "lean_str_size"]
opaque stringSize : String → USize

-- Inline C pattern (#1 = first arg, #2 = second arg)
@[extern cpp inline "#1 + #2"]
opaque fastAdd : UInt32 → UInt32 → UInt32

​
Exporting Lean Functions to C

​
The @[export] attribute

To make a Lean function callable from C, annotate it with @[export lean_symbol_name]. The name you supply becomes the exact extern "C" symbol in the generated binary. 
-- Expose a Lean function to external callers
@[export my_length]
def myLength (s : String) : UInt64 :=
  s.length.toUInt64
The resulting C declaration is: 
extern uint64_t my_length(lean_obj_arg s);
By convention, Lean’s own exported symbols use the prefix lean_. For your own libraries, choose a project-specific prefix to avoid collisions.

​
Lean’s Memory Layout: Boxed vs Unboxed Values

​
Scalar (unboxed) types

The following Lean types are passed and returned by value as their C equivalents when used in @[extern] function signatures:
Lean typeC type
UInt8uint8_t
UInt16uint16_t
UInt32uint32_t
UInt64uint64_t
USizesize_t
Floatdouble
Float32float
Booluint8_t

​
Boxed (heap-allocated) objects

Everything else — String, Array, List, user-defined structures, inductive types — is represented as a lean_object * heap pointer. The header of <lean/lean.h> defines the calling-convention typedefs: 
typedef lean_object * lean_obj_arg;    /* Standard object argument (consumes RC) */
typedef lean_object * b_lean_obj_arg;  /* Borrowed object argument (caller keeps RC) */
typedef lean_object * lean_obj_res;    /* Standard object result (caller must dec RC) */
typedef lean_object * b_lean_obj_res;  /* Borrowed object result */
Lean uses reference counting for memory management. When you receive a lean_obj_arg, you own a reference and must either pass ownership on or call lean_dec. When you receive a b_lean_obj_arg, the caller owns it and you must not decrement it unless you explicitly increment first.

​
Small scalars as tagged pointers

Non-negative integers that fit in a size_t are represented as tagged pointers: the least-significant bit is set to 1 and the value occupies the remaining bits. The runtime macros lean_box/lean_unbox convert between integers and this representation: 
static inline lean_object * lean_box(size_t n);
static inline size_t lean_unbox(lean_object * o);
static inline uint8_t lean_is_scalar(lean_object * o);

​
Working with Lean Objects from C

​
Constructors

To allocate a constructor object with tag, num_objs pointer fields, and scalar_sz bytes of scalar storage: 
#include <lean/lean.h>

// lean_alloc_ctor(tag, num_object_fields, scalar_bytes)
lean_object * mk_pair(lean_obj_arg fst, lean_obj_arg snd) {
    lean_object * o = lean_alloc_ctor(0, 2, 0);
    lean_ctor_set(o, 0, fst);
    lean_ctor_set(o, 1, snd);
    return o;
}
To read a field back: 
b_lean_obj_res lean_ctor_get(b_lean_obj_arg o, unsigned i);

// Scalar field accessors
uint32_t lean_ctor_get_uint32(b_lean_obj_arg o, unsigned offset);
uint64_t lean_ctor_get_uint64(b_lean_obj_arg o, unsigned offset);
double   lean_ctor_get_float(b_lean_obj_arg o, unsigned offset);

​
Strings and IO results

// Create a Lean String from a null-terminated C string
lean_obj_res lean_mk_string(const char * s);

// Wrap a value in IO.Result.ok
lean_obj_res lean_io_result_mk_ok(lean_obj_arg val);

// Check whether an IO result is ok
uint8_t lean_io_result_is_ok(b_lean_obj_arg r);

​
Example: a C++ function returning IO String

// ffi_shared.cpp
#include <lean/lean.h>
#include <string>

extern "C" lean_obj_res my_lean_fun() {
    std::string msg = "hello from C++";
    lean_obj_res result = lean_mk_string(msg.c_str());
    return lean_io_result_mk_ok(result);
}

-- Lean declaration
@[extern "my_lean_fun"]
opaque myLeanFun : IO String

def main : IO Unit := do
  IO.println (← myLeanFun)

​
Initializing Lean from a C main

When calling Lean from a C program (reverse FFI), you must initialize the Lean runtime and each imported module before accessing any Lean declarations: 
#include <lean/lean.h>
#include <stdio.h>

// generated symbol: initialize_<package>_<module>
extern lean_object * initialize_rffi_RFFI(uint8_t builtin);
extern void lean_io_mark_end_initialization();

// declared with @[export my_length]
extern uint64_t my_length(lean_obj_arg s);

int main() {
    uint8_t builtin = 1;
    lean_object * res = initialize_rffi_RFFI(builtin);
    if (lean_io_result_is_ok(res)) {
        lean_dec_ref(res);
    } else {
        lean_io_result_show_error(res);
        lean_dec(res);
        return 1;
    }
    lean_io_mark_end_initialization();

    lean_object * s = lean_mk_string("hello!");
    uint64_t l = my_length(s);
    printf("length: %lu\n", l);
    return 0;
}
Do not access any Lean declaration if module initialization returned an error. Always check lean_io_result_is_ok before calling exported symbols.

​
Including C Files in a Lake Package

Lake provides build targets for compiling C/C++ files and linking them into Lean libraries. Below is the pattern from the official FFI example in the Lean 4 repository: 
-- lakefile.lean
import Lake
open System Lake DSL

package ffi where
  srcDir := "lean"

lean_lib FFI

-- Compile the C source to an object file
input_file ffi_static.c where
  path := "c" / "ffi_static.c"
  text := true

target ffi_static.o pkg : FilePath := do
  let srcJob ← ffi_static.c.fetch
  let oFile := pkg.buildDir / "c" / "ffi_static.o"
  buildO oFile srcJob #[] #["-fPIC"] "cc"

-- Link the object file into a static library
target libleanffi_static pkg : FilePath := do
  let ffiO ← ffi_static.o.fetch
  let name := nameToStaticLib "leanffi"
  buildStaticLib (pkg.staticLibDir / name) #[ffiO]

-- Attach the static library to the Lean library
lean_lib FFI.Static where
  moreLinkObjs := #[libleanffi_static]
For a shared library (e.g., when the C code depends on Lean’s own shared library), replace buildStaticLib with buildSharedLib and use moreLinkLibs instead of moreLinkObjs.
If you want to use a Lean library from an external Makefile or CMake project, build the library with lake build and link against the generated lib*.a or lib*.so files. You also need to compile with -I $(lean --print-prefix)/include so that <lean/lean.h> is on the include path.See the tests/lake/examples/reverse-ffi/ directory in the Lean 4 repository for a minimal working example including a Makefile.

​
Reference: Common C API Functions

void lean_inc(lean_object * o);          // increment RC (no-op for scalars)
void lean_dec(lean_object * o);          // decrement RC, free if zero
void lean_inc_n(lean_object * o, size_t n);
lean_object * lean_box(size_t n);        // encode small integer
size_t lean_unbox(lean_object * o);      // decode small integer
uint8_t lean_is_scalar(lean_object * o); // true iff tagged pointer

lean_object * lean_alloc_ctor(unsigned tag, unsigned num_objs, unsigned scalar_sz);
b_lean_obj_res lean_ctor_get(b_lean_obj_arg o, unsigned i);
void lean_ctor_set(b_lean_obj_arg o, unsigned i, lean_obj_arg v);
uint8_t  lean_ctor_get_uint8(b_lean_obj_arg o, unsigned offset);
uint32_t lean_ctor_get_uint32(b_lean_obj_arg o, unsigned offset);
uint64_t lean_ctor_get_uint64(b_lean_obj_arg o, unsigned offset);
double   lean_ctor_get_float(b_lean_obj_arg o, unsigned offset);
void lean_ctor_set_uint32(b_lean_obj_arg o, unsigned offset, uint32_t v);
void lean_ctor_set_uint64(b_lean_obj_arg o, unsigned offset, uint64_t v);

lean_obj_res lean_mk_string(const char * s);
lean_obj_res lean_mk_string_from_bytes(const char * s, size_t sz);
const char * lean_string_cstr(b_lean_obj_arg s);
size_t lean_string_size(b_lean_obj_arg s); // byte length + 1 (includes null terminator)

Build docs developers (and LLMs) love

Get started for freeTalk to us