lean_rs/handle/
mod.rs

1//! Opaque, lifetime-bound handles for core Lean semantic values.
2//!
3//! [`LeanName`], [`LeanLevel`], [`LeanExpr`], and [`LeanDeclaration`] are
4//! receipts for owned Lean values; each wraps a crate-internal owned-
5//! object handle so the `'lean` parameter cascades from
6//! [`crate::LeanRuntime::init`] and the underlying refcount obligation is
7//! honoured automatically. Construction and inspection live on the Lean
8//! side: the Rust handle has no public methods to mint, decode, or compare
9//! the value it carries — those operations require knowledge of Lean
10//! constructor layout, which by charter belongs to Lean code, not to this
11//! crate.
12//!
13//! ## How to use a handle
14//!
15//! Reach into Lean through [`crate::module::LeanModule::exported`]; the
16//! handle types already implement the (sealed) [`crate::module::LeanAbi`]
17//! trait so they can appear as argument or return types in the typed
18//! dispatch:
19//!
20//! ```ignore
21//! let n: LeanName = module
22//!     .exported::<((),), LeanName>("lean_rs_fixture_name_anonymous")?
23//!     .call(())?;
24//! let s: String = module
25//!     .exported::<(LeanName,), String>("lean_rs_fixture_name_to_string")?
26//!     .call(n)?;
27//! ```
28//!
29//! ## Display text is diagnostic, not a semantic key
30//!
31//! Any string a handle yields through a Lean-authored export (`toString`,
32//! a pretty-printer, a structured-format helper) is a *diagnostic*. Two
33//! values that print the same may not be the same Lean value; two values
34//! that print differently may compare equal by Lean's notion of equality
35//! at a different reduction depth or with different metadata. Use a
36//! Lean-authored equality export (e.g. `Name.beq`, `Expr.beq`) when
37//! semantics matter, not string comparison.
38//!
39//! ## Threading
40//!
41//! Every handle is `!Send + !Sync`, inherited from the crate-internal
42//! owned-object handle it wraps. Worker threads attach to Lean through
43//! the crate-internal thread-guard machinery; handles created on one
44//! thread stay on that thread.
45
46mod declaration;
47mod expr;
48mod level;
49mod name;
50
51pub use self::declaration::LeanDeclaration;
52pub use self::expr::LeanExpr;
53pub use self::level::LeanLevel;
54pub use self::name::LeanName;
55
56#[cfg(test)]
57mod tests;
lean_rs/handle/mod.rs

lean_rs/handle/
mod.rs
