Struct LeanCapabilities 

pub struct LeanCapabilities<'lean, 'h> { /* private fields */ }

Loaded capability, generic interop, and host shim dylibs with session symbol addresses pre-resolved.

Owns the LeanLibrary handles so callers do not have to track the dylibs’ lifetimes separately. Borrows from the parent LeanHost for the runtime + project context. Neither Send nor Sync: inherited from the contained LeanLibrary handles.

Implementations

impl<'lean, 'h> LeanCapabilities<'lean, 'h>

pub fn session<'c>( &'c self, imports: &[&str], cancellation: Option<&LeanCancellationToken>, progress: Option<&dyn LeanProgressSink>, ) -> LeanResult<LeanSession<'lean, 'c>>

Import the named modules into a fresh Lean environment and return a session over the result.

Imports happen exactly once per session() call. The returned LeanSession owns the imported environment and reuses this capability’s cached symbol addresses for every query.

Errors

Returns lean_rs::LeanError::Cancelled if cancellation is already cancelled before import dispatch.

Returns lean_rs::LeanError::LeanException if the Lean-side import raises (missing .olean, malformed module name, …), with the bounded message Lean surfaced.

Trait Implementations

impl Debug for LeanCapabilities<'_, '_>

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

Formats the value using the given formatter.