Struct LeanModule 

pub struct LeanModule<'lean, 'lib> { /* private fields */ }

A Lean module that has been linked and initialized successfully.

Holds a borrow of its source LeanLibrary; the 'lib lifetime keeps the dylib loaded while any LeanModule referring to it is alive. The 'lean lifetime is inherited from the library, which inherits it from the crate::LeanRuntime borrow that anchored the whole chain. Neither Send nor Sync (inherited from the &LeanLibrary field).

Implementations

impl<'lean, 'lib> LeanModule<'lean, 'lib>

pub unsafe fn exported_unchecked<Args, R>( &self, name: &str, ) -> LeanResult<LeanExported<'lean, 'lib, Args, R>>

where Args: LeanArgs<'lean>, R: DecodeCallResult<'lean>,

Look up a typed handle for the named exported symbol without ABI metadata checks.

Args is a tuple of Rust argument types whose arity matches the Lean export’s parameter count (use () for nullary exports); each element must implement LeanAbi. R is the return decoder: either a LeanAbi type (pure path) or LeanIo<T> for an IO α-returning export.

Safety

The caller must prove that name resolves to a Lean export whose emitted C ABI and ownership behavior exactly match the requested Rust Args and R:

• each argument slot must have the C representation selected by that slot’s LeanAbi::CRepr, in the same order and arity;
• the return slot must have the C representation expected by DecodeCallResult::CRepr, including LeanIo<T> only for exports that return Lean IO α;
• object arguments and results must follow Lake’s ownership and refcount transfer rules for the chosen signature.

Passing a Rust signature that does not match the Lean export’s actual C ABI is undefined behavior.

Errors

Returns LeanError::Host with stage HostStage::Link if:

• the symbol is not exported by this module’s library;
• the symbol is a Lean nullary-constant global (data-section symbol) and Args::ARITY > 0—the function-vs-global mismatch is diagnosed at lookup so the next .call cannot SIGBUS;
• the symbol is a Lean nullary-constant global and R is LeanIo<_>—globals are never IO-returning in Lean, so the decoder cannot apply.

impl<'lean, 'lib> LeanModule<'lean, 'lib>

pub fn module_name(&self) -> &str

Human-readable package::Module.Path form for diagnostics.

The format matches what crate::module::LeanLibrary::initialize_module accepted, so log messages and test assertions can round-trip the name a caller used.

Trait Implementations

impl Debug for LeanModule<'_, '_>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.