Struct LeanExported 

pub struct LeanExported<'lean, 'lib, Args, R> { /* private fields */ }

A typed handle for an exported Lean symbol.

Holds a resolved symbol address (function or persistent global) and the runtime borrow that anchors any Obj it produces. Construction goes exclusively through LeanModule::exported; the handle borrows from its source LeanModule via 'lib so neither the library nor the runtime can be dropped while a handle is live.

Args is a tuple of Rust argument types whose elements implement LeanAbi; the LeanArgs impl for that tuple supplies the arity. R is the return type, satisfying DecodeCallResult.

Neither Send nor Sync: the contained runtime reference and the *mut symbol address both propagate the per-thread restriction.

Implementations

impl<'lean, Args, R> LeanExported<'lean, '_, Args, R>

pub unsafe fn from_function_address( runtime: &'lean LeanRuntime, address: *mut c_void, ) -> Self

Build a function-targeted typed handle from a pre-resolved symbol address.

LeanModule::exported is the normal lookup path; this constructor exists so external opinionated host stacks (e.g. lean-rs-host’s LeanCapabilities) can pre-resolve a capability dylib’s function symbols once at load time via LeanLibrary::resolve_function_symbol and then dispatch through cached addresses without re-dlsym-ing per call. It always produces a Function-targeted handle — global symbols still go through LeanModule::exported.

Safety

The caller must guarantee all of the following:

• address is the entry point of a function in a library that outlives 'lib (typically a &'lib LeanLibrary<'lean>).
• The function’s C ABI matches the requested Args / R shape under Lake’s emission conventions (per-arg LeanAbi::CRepr, per-result DecodeCallResult::CRepr).
• runtime is the witness for 'lean.

impl<'lean, 'lib, R> LeanExported<'lean, 'lib, (), R>

where R: DecodeCallResult<'lean>,

pub fn call(&self) -> LeanResult<R::Output>

Invoke the exported symbol and decode the result.

Errors

Returns LeanError::LeanException when the underlying Lean export raises through IO (only possible when R is LeanIo<_>). Returns LeanError::Host with stage HostStage::Conversion when the return value does not decode into the declared R type.

impl<'lean, 'lib, A1, R> LeanExported<'lean, 'lib, (A1,), R>

where A1: LeanAbi<'lean>, R: DecodeCallResult<'lean>,

pub fn call(&self, a1: A1) -> LeanResult<R::Output>

Invoke the exported symbol and decode the result.

Errors

Returns LeanError::LeanException when the underlying Lean export raises through IO (only possible when R is LeanIo<_>). Returns LeanError::Host with stage HostStage::Conversion when the return value does not decode into the declared R type.

impl<'lean, 'lib, A1, A2, R> LeanExported<'lean, 'lib, (A1, A2), R>

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, R: DecodeCallResult<'lean>,

pub fn call(&self, a1: A1, a2: A2) -> LeanResult<R::Output>

Invoke the exported symbol and decode the result.

Errors

Returns LeanError::LeanException when the underlying Lean export raises through IO (only possible when R is LeanIo<_>). Returns LeanError::Host with stage HostStage::Conversion when the return value does not decode into the declared R type.

impl<'lean, 'lib, A1, A2, A3, R> LeanExported<'lean, 'lib, (A1, A2, A3), R>

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, R: DecodeCallResult<'lean>,

pub fn call(&self, a1: A1, a2: A2, a3: A3) -> LeanResult<R::Output>

Invoke the exported symbol and decode the result.

Errors

Returns LeanError::LeanException when the underlying Lean export raises through IO (only possible when R is LeanIo<_>). Returns LeanError::Host with stage HostStage::Conversion when the return value does not decode into the declared R type.

impl<'lean, 'lib, A1, A2, A3, A4, R> LeanExported<'lean, 'lib, (A1, A2, A3, A4), R>

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>, R: DecodeCallResult<'lean>,

pub fn call(&self, a1: A1, a2: A2, a3: A3, a4: A4) -> LeanResult<R::Output>

Invoke the exported symbol and decode the result.

Errors

Returns LeanError::LeanException when the underlying Lean export raises through IO (only possible when R is LeanIo<_>). Returns LeanError::Host with stage HostStage::Conversion when the return value does not decode into the declared R type.

impl<'lean, 'lib, A1, A2, A3, A4, A5, R> LeanExported<'lean, 'lib, (A1, A2, A3, A4, A5), R>

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>, A5: LeanAbi<'lean>, R: DecodeCallResult<'lean>,

pub fn call( &self, a1: A1, a2: A2, a3: A3, a4: A4, a5: A5, ) -> LeanResult<R::Output>

Invoke the exported symbol and decode the result.

Errors

Returns LeanError::LeanException when the underlying Lean export raises through IO (only possible when R is LeanIo<_>). Returns LeanError::Host with stage HostStage::Conversion when the return value does not decode into the declared R type.

impl<'lean, 'lib, A1, A2, A3, A4, A5, A6, R> LeanExported<'lean, 'lib, (A1, A2, A3, A4, A5, A6), R>

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>, A5: LeanAbi<'lean>, A6: LeanAbi<'lean>, R: DecodeCallResult<'lean>,

pub fn call( &self, a1: A1, a2: A2, a3: A3, a4: A4, a5: A5, a6: A6, ) -> LeanResult<R::Output>

Invoke the exported symbol and decode the result.

Errors

Returns LeanError::LeanException when the underlying Lean export raises through IO (only possible when R is LeanIo<_>). Returns LeanError::Host with stage HostStage::Conversion when the return value does not decode into the declared R type.

impl<'lean, 'lib, A1, A2, A3, A4, A5, A6, A7, R> LeanExported<'lean, 'lib, (A1, A2, A3, A4, A5, A6, A7), R>

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>, A5: LeanAbi<'lean>, A6: LeanAbi<'lean>, A7: LeanAbi<'lean>, R: DecodeCallResult<'lean>,

pub fn call( &self, a1: A1, a2: A2, a3: A3, a4: A4, a5: A5, a6: A6, a7: A7, ) -> LeanResult<R::Output>

Invoke the exported symbol and decode the result.

Errors

Returns LeanError::LeanException when the underlying Lean export raises through IO (only possible when R is LeanIo<_>). Returns LeanError::Host with stage HostStage::Conversion when the return value does not decode into the declared R type.

impl<'lean, 'lib, A1, A2, A3, A4, A5, A6, A7, A8, R> LeanExported<'lean, 'lib, (A1, A2, A3, A4, A5, A6, A7, A8), R>

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>, A5: LeanAbi<'lean>, A6: LeanAbi<'lean>, A7: LeanAbi<'lean>, A8: LeanAbi<'lean>, R: DecodeCallResult<'lean>,

pub fn call( &self, a1: A1, a2: A2, a3: A3, a4: A4, a5: A5, a6: A6, a7: A7, a8: A8, ) -> LeanResult<R::Output>

Invoke the exported symbol and decode the result.

Errors

Returns LeanError::LeanException when the underlying Lean export raises through IO (only possible when R is LeanIo<_>). Returns LeanError::Host with stage HostStage::Conversion when the return value does not decode into the declared R type.

impl<'lean, 'lib, A1, A2, A3, A4, A5, A6, A7, A8, A9, R> LeanExported<'lean, 'lib, (A1, A2, A3, A4, A5, A6, A7, A8, A9), R>

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>, A5: LeanAbi<'lean>, A6: LeanAbi<'lean>, A7: LeanAbi<'lean>, A8: LeanAbi<'lean>, A9: LeanAbi<'lean>, R: DecodeCallResult<'lean>,

pub fn call( &self, a1: A1, a2: A2, a3: A3, a4: A4, a5: A5, a6: A6, a7: A7, a8: A8, a9: A9, ) -> LeanResult<R::Output>

Invoke the exported symbol and decode the result.

Errors

Returns LeanError::LeanException when the underlying Lean export raises through IO (only possible when R is LeanIo<_>). Returns LeanError::Host with stage HostStage::Conversion when the return value does not decode into the declared R type.

impl<'lean, 'lib, A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, R> LeanExported<'lean, 'lib, (A1, A2, A3, A4, A5, A6, A7, A8, A9, A10), R>

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>, A5: LeanAbi<'lean>, A6: LeanAbi<'lean>, A7: LeanAbi<'lean>, A8: LeanAbi<'lean>, A9: LeanAbi<'lean>, A10: LeanAbi<'lean>, R: DecodeCallResult<'lean>,

pub fn call( &self, a1: A1, a2: A2, a3: A3, a4: A4, a5: A5, a6: A6, a7: A7, a8: A8, a9: A9, a10: A10, ) -> LeanResult<R::Output>

Invoke the exported symbol and decode the result.

Errors

Returns LeanError::LeanException when the underlying Lean export raises through IO (only possible when R is LeanIo<_>). Returns LeanError::Host with stage HostStage::Conversion when the return value does not decode into the declared R type.

impl<'lean, 'lib, A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, R> LeanExported<'lean, 'lib, (A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11), R>

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>, A5: LeanAbi<'lean>, A6: LeanAbi<'lean>, A7: LeanAbi<'lean>, A8: LeanAbi<'lean>, A9: LeanAbi<'lean>, A10: LeanAbi<'lean>, A11: LeanAbi<'lean>, R: DecodeCallResult<'lean>,

pub fn call( &self, a1: A1, a2: A2, a3: A3, a4: A4, a5: A5, a6: A6, a7: A7, a8: A8, a9: A9, a10: A10, a11: A11, ) -> LeanResult<R::Output>

Invoke the exported symbol and decode the result.

Errors

Returns LeanError::LeanException when the underlying Lean export raises through IO (only possible when R is LeanIo<_>). Returns LeanError::Host with stage HostStage::Conversion when the return value does not decode into the declared R type.

impl<'lean, 'lib, A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, R> LeanExported<'lean, 'lib, (A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12), R>

where A1: LeanAbi<'lean>, A2: LeanAbi<'lean>, A3: LeanAbi<'lean>, A4: LeanAbi<'lean>, A5: LeanAbi<'lean>, A6: LeanAbi<'lean>, A7: LeanAbi<'lean>, A8: LeanAbi<'lean>, A9: LeanAbi<'lean>, A10: LeanAbi<'lean>, A11: LeanAbi<'lean>, A12: LeanAbi<'lean>, R: DecodeCallResult<'lean>,

pub fn call( &self, a1: A1, a2: A2, a3: A3, a4: A4, a5: A5, a6: A6, a7: A7, a8: A8, a9: A9, a10: A10, a11: A11, a12: A12, ) -> LeanResult<R::Output>

Invoke the exported symbol and decode the result.

Errors

Returns LeanError::LeanException when the underlying Lean export raises through IO (only possible when R is LeanIo<_>). Returns LeanError::Host with stage HostStage::Conversion when the return value does not decode into the declared R type.

Trait Implementations

impl<Args, R> Debug for LeanExported<'_, '_, Args, R>

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

Formats the value using the given formatter.