Module module 

Loading and initializing compiled Lean modules.

The normal shipped-capability path is LeanCapability, which stores a LeanLibraryBundle internally. The lower-level surface has three RAII types:

• LeanLibrary — a Lake-built native shared object opened through the platform dynamic loader.
• LeanLibraryBundle — a primary shared object plus dependent Lean dylibs anchored for the same lifetime.
• LeanModule — proof that a named Lean module hosted by a LeanLibrary has been initialized to IO.ok(()).
• LeanCapabilityPreflight — manifest and artifact checks that turn package/loader failures into stable repair hints before opening.

Construction of either type requires a crate::LeanRuntime borrow, so use-before-init is structurally impossible. The 'lean lifetime cascade keeps every derived handle bound to the runtime witness; the secondary 'lib lifetime on LeanModule keeps initialized modules from outliving the dylib that hosts them.

let runtime = lean_rs::LeanRuntime::init()?;
let library = lean_rs::module::LeanLibrary::open(runtime, "path/to/libfoo.dylib")?;
let module  = library.initialize_module("foo_pkg", "Foo.Bar")?;

Callers do not name raw initializer symbols, choose the Lean builtin flag, decode IO results, or maintain idempotency state; all of that lives in the pub(crate) module::initializer infrastructure. Typed exported-function handles cross the public boundary as LeanExported and LeanIo; see exported for the call shape.

Re-exports

pub use crate::abi::traits::LeanAbi;

Structs

LeanBuiltCapability

Runtime descriptor for a Lean capability built by a downstream build.rs.

LeanCapability

Opened Lean capability whose dylib path and initializer names came from the build-script pairing.

LeanCapabilityPreflight

Preflight runner for manifest-backed Lean capabilities.

LeanExported

A typed handle for an exported Lean symbol.

LeanIo

Return-type marker for Lean exports declared IO α.

LeanLibrary

A loaded native Lean shared object.

LeanLibraryBundle

A primary Lean capability plus its dependent Lean dylibs.

LeanLibraryDependency

Dependency dylib that must stay alive while a capability is loaded.

LeanLoaderCheck

One bounded preflight finding.

LeanLoaderReport

Structured result of loader preflight for one capability manifest.

LeanModule

A Lean module that has been linked and initialized successfully.

LeanModuleInitializer

Initializer for a Lean module hosted by a loaded dylib.

Enums

LeanLoaderDiagnosticCode

Stable preflight diagnostic codes for manifest-backed capability loading.

LeanLoaderSeverity

Severity of one loader preflight finding.

Traits

DecodeCallResult

How to decode an owned Lean call result into a Rust value.

LeanArgs

Per-arity marker for LeanExported’s argument tuple.