Basic Example

This walkthrough builds the smallest possible lean-py project: a handful of functions, a structure, and an inductive type, all callable from Python.

View full source on GitHub

The Lean side

We start with the imports. Every lean-py project needs import LeanPy:

import LeanPy
open LeanPy

Exporting a function

The simplest thing you can do is export a function. Annotate it with @[python "symbol_name"] and lean-py takes care of the rest – type marshalling, C ABI, everything:

@[python "py_increment"]
def increment (x : Int) : Int := x + 1

On the Python side, this becomes lib.increment(7) and returns 8.

Functions can return IO too. lean-py unwraps the IO result automatically (and raises LeanError on failure):

@[python "py_greet"]
def greet (name : String) : IO String :=
  return s!"Hello, {name}!"

Collection types like Array are marshalled to Python lists:

@[python "py_sum_array"]
def sumArray (xs : Array Int) : Int :=
  xs.foldl (· + ·) 0

Exporting a structure

Structures need one extra step: derive_python registers the type’s constructor so Python can both create and destructure values:

structure Point where
  x : Int
  y : Int
  deriving Repr

derive_python Point

Now you can export functions that take or return Point:

@[python "py_origin"]
def origin (_ : Unit) : Point := ⟨0, 0⟩

@[python "py_norm_sq"]
def normSq (p : Point) : Int := p.x * p.x + p.y * p.y

Exporting an inductive

Inductives work the same way. Each constructor becomes accessible on the Python side as an attribute of the type:

inductive Shape where
  | circle (r : Int)
  | square (side : Int)
  | rect   (w h : Int)
  deriving Repr

derive_python Shape

@[python "py_perimeter"]
def perimeter (s : Shape) : Int :=
  match s with
  | .circle r => 6 * r
  | .square s => 4 * s
  | .rect w h => 2 * (w + h)

Making it all visible

The last line in the Lean file is what actually makes everything discoverable by Python:

#export_python_registry "Basic"

This emits two C functions (Basic_funcs_json and Basic_types_json) that LeanLibrary reads at load time to build wrappers.

The Python side

After lake build, the Python code is straightforward:

from lean_py import LeanLibrary

lib = LeanLibrary.from_lake("path/to/lean", "Basic", build=True)

Now call everything we exported:

>>> lib.increment(7)
8

>>> lib.greet("world")
'Hello, world!'

>>> lib.sumArray(list(range(1, 11)))
55

Structures are callable – lib.Point(3, 4) constructs a LeanInductiveValue that can be passed back to Lean:

>>> p = lib.Point(3, 4)
>>> p
Point.mk(3, 4)

>>> lib.normSq(p)
25

Inductives expose their constructors as attributes:

>>> lib.Shape.circle(5)
Shape.circle(5)

>>> lib.perimeter(lib.Shape.circle(5))
30

>>> lib.perimeter(lib.Shape.rect(2, 3))
10

Pattern matching works naturally with Python 3.10+ match/case:

Shape = lib.Shape

def describe(s):
    match s:
        case Shape.circle(r):
            return f"circle with radius {r}"
        case Shape.square(side):
            return f"square with side {side}"
        case Shape.rect(w, h):
            return f"{w}x{h} rectangle"

>>> describe(lib.Shape.circle(5))
'circle with radius 5'

>>> describe(lib.Shape.rect(2, 3))
'2x3 rectangle'

Running it

cd examples/01_basic/lean && lake build && cd ..
uv run --project python python/main.py

Output:

py_increment(7)        = 8
py_greet("world")      = Hello, world!
py_sum_array([1..10])  = 55
py_origin(())          = Point.mk(0, 0)
py_norm_sq((3, 4))     = 25
py_perimeter(circle 5) = 30
py_perimeter(square 4) = 16
py_perimeter(rect 2 3) = 10

What to take away

Three annotations power the whole thing:

1. @[python "name"] – export a function.

2. derive_python T – register a type’s constructors.

3. #export_python_registry "Prefix" – emit the metadata Python reads.

On the Python side, LeanLibrary.from_lake(...) does all the work: finding the shared library, calling the JSON registry, and building typed wrappers.