Struct LeanLevel 

pub struct LeanLevel<'lean> { /* private fields */ }

Opaque, lifetime-bound handle to a Lean.Level.

'lean cascades from the crate::LeanRuntime borrow that produced the value, so a handle cannot outlive the runtime. Neither Send nor Sync: inherited from the crate-internal owned-object handle the type wraps.

Clone bumps the underlying refcount; Drop releases it. There are no public inherent methods: the handle is a pass-through that reaches Lean-authored operations through crate::module::LeanModule::exported.

Trait Implementations

impl Clone for LeanLevel<'_>

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanLevel<'_>

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

Formats the value using the given formatter.

impl<'lean> LeanAbi<'lean> for LeanLevel<'lean>

type CRepr = *mut lean_object

The C-ABI type Lake emits for this Lean type at function signatures.

impl<'lean> TryFromLean<'lean> for LeanLevel<'lean>

fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self>

Decode obj into Self, returning a LeanError::Host with stage HostStage::Conversion if the object’s kind or payload is outside the type’s representable range.