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_unchecked; 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, '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.