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 fn exported<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.

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.

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.