Module handle 

Opaque, lifetime-bound handles for core Lean semantic values.

LeanName, LeanLevel, LeanExpr, and LeanDeclaration are receipts for owned Lean values; each wraps a crate-internal owned- object handle so the 'lean parameter cascades from crate::LeanRuntime::init and the underlying refcount obligation is honoured automatically. Construction and inspection live on the Lean side: the Rust handle has no public methods to mint, decode, or compare the value it carries — those operations require knowledge of Lean constructor layout, which by charter belongs to Lean code, not to this crate.

How to use a handle

Reach into Lean through crate::module::LeanModule::exported; the handle types already implement the (sealed) crate::module::LeanAbi trait so they can appear as argument or return types in the typed dispatch:

let n: LeanName = module
    .exported::<((),), LeanName>("lean_rs_fixture_name_anonymous")?
    .call(())?;
let s: String = module
    .exported::<(LeanName,), String>("lean_rs_fixture_name_to_string")?
    .call(n)?;

Display text is diagnostic, not a semantic key

Any string a handle yields through a Lean-authored export (toString, a pretty-printer, a structured-format helper) is a diagnostic. Two values that print the same may not be the same Lean value; two values that print differently may compare equal by Lean’s notion of equality at a different reduction depth or with different metadata. Use a Lean-authored equality export (e.g. Name.beq, Expr.beq) when semantics matter, not string comparison.

Threading

Every handle is !Send + !Sync, inherited from the crate-internal owned-object handle it wraps. Worker threads attach to Lean through the crate-internal thread-guard machinery; handles created on one thread stay on that thread.

Structs

LeanDeclaration

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

LeanExpr

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

LeanLevel

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

LeanName

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