Expand description
Typed first-order ABI conversions for lean-rs.
The public surface is the sealed LeanAbi trait
(re-exported at the crate root) plus the unboxing/boxing impls for
every Lean type that crosses crate::module::LeanExported’s typed
dispatch. Sealing prevents downstream crates from implementing
LeanAbi for foreign types — wrong impls would produce undefined
behaviour at the FFI boundary.
The submodules (nat, structure, traits) expose the
helpers the sibling lean-rs-host crate needs to decode and
construct host-defined Lean structures; their items are reachable
via lean_rs::__host_internals and are not part of lean-rs’s
public semver promise.