Crate lean_rs_abi 

Link-free Lean 4 ABI and toolchain metadata.

This crate owns the static metadata that both build tooling and raw FFI bindings need: the supported Lean toolchain window, the required Lean runtime symbol names, and the lean.h layout constants. It is purely static — no build script, no extern "C" items, no link directives, and no probe of an installed toolchain — so any crate can depend on it without a Lean toolchain present. Live toolchain identity (installed version, header path, header digest) belongs to lean-toolchain, the crate whose job is toolchain discovery.

Re-exports

pub use consts::LEAN_ARRAY;

pub use consts::LEAN_CLOSURE;

pub use consts::LEAN_CLOSURE_MAX_ARGS;

pub use consts::LEAN_EXTERNAL;

pub use consts::LEAN_MAX_CTOR_FIELDS;

pub use consts::LEAN_MAX_CTOR_SCALARS_SIZE;

pub use consts::LEAN_MAX_CTOR_TAG;

pub use consts::LEAN_MAX_SMALL_OBJECT_SIZE;

pub use consts::LEAN_MPZ;

pub use consts::LEAN_OBJECT_SIZE_DELTA;

pub use consts::LEAN_PROMISE;

pub use consts::LEAN_REF;

pub use consts::LEAN_RESERVED;

pub use consts::LEAN_SCALAR_ARRAY;

pub use consts::LEAN_STRING;

pub use consts::LEAN_STRUCT_ARRAY;

pub use consts::LEAN_TASK;

pub use consts::LEAN_THUNK;

pub use supported::SUPPORTED_TOOLCHAINS;

pub use supported::SupportedToolchain;

pub use supported::supported_by_digest;

pub use supported::supported_for;

pub use supported::symbol_present_in_window;

Modules

consts

Static lean.h layout constants: object tag bytes, allocator ceilings, and constructor-shape limits.

supported

The supported Lean toolchain window.

Constants

REQUIRED_SYMBOLS

VERSION

Version of the lean-rs-abi crate, matching Cargo.toml.

Functions

symbol_in_all

Return true iff symbol is required and present across the window.