Struct Lean 

pub struct Lean<'l> { /* private fields */ }

A token that proves the Lean runtime is initialized.

This type is used throughout Leo3 to ensure that Lean objects are only accessed when the runtime is properly initialized. The 'l lifetime parameter ties all Lean objects to the initialization scope.

Example

use leo3::prelude::*;

fn process_data<'l>(lean: Lean<'l>) -> LeanResult<()> {
    // Create Lean objects using the token
    let s = LeanString::mk(lean, "Hello");
    Ok(())
}

Safety

The Lean<'l> token is typically created by with_lean() or similar functions that ensure proper initialization. Users should not create this token manually except in very specific circumstances.

Implementations

impl<'l> Lean<'l>

pub unsafe fn assume_initialized() -> Self

Create a new Lean<'l> token.

Safety

The caller must ensure that the Lean runtime is properly initialized before calling this function. This is typically done by calling prepare_freethreaded_lean().

This function should generally not be called directly by users. Use with_lean() instead.

pub fn as_ptr(self) -> *mut c_void

Get a pointer to the Lean runtime context.

This is used internally for FFI calls that require context. Most users won’t need to call this directly.

Trait Implementations

impl<'l> Clone for Lean<'l>

fn clone(&self) -> Lean<'l>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'l> Copy for Lean<'l>