Crate leo3 

Leo3: Rust bindings for the Lean4 theorem prover

Leo3 provides safe, ergonomic Rust bindings to Lean4, similar to how PyO3 provides Python bindings for Rust.

Architecture

Leo3 is organized into several layers:

• leo3-ffi: Raw FFI bindings to Lean4’s C API
• leo3-build-config: Build-time configuration and Lean4 detection
• leo3-macros: Procedural macros (#[leanfn], etc.)
• leo3 (this crate): Safe, high-level abstractions

Core Concepts

The Lean<'l> Token

All interactions with Lean require a Lean<'l> token, which proves at compile-time that the Lean runtime is initialized. This prevents accessing Lean objects without proper initialization.

Smart Pointers

Leo3 provides several smart pointer types:

• LeanBound<'l, T>: A Lean object bound to a Lean<'l> lifetime
• LeanRef<T>: An owned reference to a Lean object (can cross initialization boundaries)
• LeanBorrowed<'a, 'l, T>: A borrowed reference (zero-cost)
• LeanUnbound<T>: A thread-safe reference with automatic MT marking (Send + Sync)

Reference Counting

Lean4 uses reference counting for memory management. Leo3’s smart pointers automatically handle reference counting to prevent memory leaks and use-after-free.

Thread Safety

Lean4 uses a dual-mode reference counting system:

• ST (Single-Threaded): Non-atomic, faster reference counting
• MT (Multi-Threaded): Atomic reference counting for thread safety

Use LeanUnbound<T> or unbind_mt() for objects that need to cross thread boundaries.

Feature Flags

• macros (default): Enable procedural macros (#[leanfn], etc.)

Example

use leo3::prelude::*;

#[leanfn]
fn add(a: u64, b: u64) -> u64 {
    a + b
}

fn main() -> LeanResult<()> {
    leo3::prepare_freethreaded_lean();

    leo3::with_lean(|lean| {
        // Use Lean objects here
        let result = add(2, 3);
        println!("Result: {}", result);
        Ok(())
    })
}

Re-exports

pub use err::KernelExceptionCode;

pub use err::LeanError;

pub use err::LeanResult;

pub use instance::LeanBorrowed;

pub use instance::LeanBound;

pub use instance::LeanRef;

pub use marker::Lean;

pub use unbound::LeanUnbound;

pub use leo3_ffi as ffi;

Modules

closure

Safe wrapper for Lean closures.

conversion

Traits for converting between Rust and Lean types.

err

Error types for Leo3.

external

External objects for wrapping Rust types in Lean4.

instance

Smart pointers for managing Lean objects.

io

IO operations for Lean4.

marker

The Lean<'l> token for compile-time Lean runtime verification.

meta

Meta-programming module for Leo3

module

Dynamic loading and calling of Lean4 compiled functions

prelude

Prelude module for convenient imports

promise

Safe wrapper for Lean promises (manually-resolvable async values).

sync

Synchronization primitives for thread-safe Lean object access.

task

Safe wrapper for Lean tasks (parallel computation).

task_combinators

Async combinators for Lean tasks.

thunk

Safe wrapper for Lean thunks (lazy evaluation).

tokio_bridgetokio

Optional Tokio integration for Lean tasks.

types

Wrappers for Lean built-in types.

unbound

Thread-safe smart pointer for Lean objects.

Macros

from_lean

Macro for automatic conversion from Lean. For Vec<u8>, uses optimized conversion. For other types, delegates to FromLean trait.

to_lean

Macro for automatic conversion dispatch. For Vec<u8> and &[u8], uses optimized bulk memcpy. For other types, delegates to IntoLean trait.

Functions

prepare_freethreaded_lean

Initialize the Lean runtime for standalone use.

test_with_lean

Execute a test with proper Lean thread lifecycle management.

with_lean

Execute a closure with access to the Lean runtime.