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_unchecked`]; 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//! // SAFETY: the Lean fixture pins this export as `Unit -> Name`.
22//! let mk_name = unsafe {
23//!     module.exported_unchecked::<((),), LeanName>("lean_rs_fixture_name_anonymous")
24//! }?;
25//! let n: LeanName = mk_name.call(())?;
26//!
27//! // SAFETY: the Lean fixture pins this export as `Name -> String`.
28//! let name_to_string = unsafe {
29//!     module.exported_unchecked::<(LeanName,), String>("lean_rs_fixture_name_to_string")
30//! }?;
31//! let s: String = name_to_string.call(n)?;
32//! ```
33//!
34//! ## Display text is diagnostic, not a semantic key
35//!
36//! Any string a handle yields through a Lean-authored export (`toString`,
37//! a pretty-printer, a structured-format helper) is a *diagnostic*. Two
38//! values that print the same may not be the same Lean value; two values
39//! that print differently may compare equal by Lean's notion of equality
40//! at a different reduction depth or with different metadata. Use a
41//! Lean-authored equality export (e.g. `Name.beq`, `Expr.beq`) when
42//! semantics matter, not string comparison.
43//!
44//! ## Threading
45//!
46//! Every handle is `!Send + !Sync`, inherited from the crate-internal
47//! owned-object handle it wraps. Worker threads attach to Lean through
48//! the crate-internal thread-guard machinery; handles created on one
49//! thread stay on that thread.
50
51mod declaration;
52mod expr;
53mod level;
54mod name;
55
56pub use self::declaration::LeanDeclaration;
57pub use self::expr::LeanExpr;
58pub use self::level::LeanLevel;
59pub use self::name::LeanName;
60
61#[cfg(test)]
62mod tests;
lean_rs/handle/mod.rs

lean_rs/handle/
mod.rs
