lean_rs/abi/
mod.rs

1//! Typed first-order ABI conversions for `lean-rs`.
2//!
3//! The public surface is the sealed [`LeanAbi`](traits::LeanAbi) trait
4//! (re-exported at the crate root) plus the unboxing/boxing impls for
5//! every Lean type that crosses [`crate::module::LeanExported`]'s typed
6//! dispatch. Sealing prevents downstream crates from implementing
7//! `LeanAbi` for foreign types — wrong impls would produce undefined
8//! behaviour at the FFI boundary.
9//!
10//! The submodules ([`nat`], [`structure`], [`traits`]) expose the
11//! helpers the sibling `lean-rs-host` crate needs to decode and
12//! construct host-defined Lean structures; their items are reachable
13//! via `lean_rs::__host_internals` and are not part of `lean-rs`'s
14//! public semver promise.
15
16// Items here are infrastructure for the typed `LeanExported` family
17// and the `module` / `host` modules. A subset is exercised only by
18// `cargo test` (the in-tree `abi::tests` and the integration suites);
19// the lib-only `cargo build` cannot prove every helper is reachable.
20#![allow(
21    dead_code,
22    reason = "ABI helpers reached through generic dispatch; lib-only build cannot prove reachability"
23)]
24
25pub(crate) mod array;
26pub(crate) mod bytearray;
27pub(crate) mod except;
28pub(crate) mod int;
29pub mod nat;
30pub(crate) mod option;
31pub(crate) mod scalar;
32pub(crate) mod string;
33pub mod structure;
34pub mod traits;
35pub(crate) mod tuple;
36
37#[cfg(test)]
38mod tests;
lean_rs/abi/mod.rs

lean_rs/abi/
mod.rs
