Module supported 

The supported Lean toolchain window.

lean-rs-sys accepts the active toolchain at build time iff its lean.h digest matches one entry in SUPPORTED_TOOLCHAINS. The table is the single source of truth for the v1.0 compatibility promise.

Each entry records the SHA-256 of one include/lean/lean.h, the LEAN_VERSION_STRING values that ship that exact header (Lean does not always bump the header between releases — header-identical releases share one entry), and the set of REQUIRED_SYMBOLS that are absent from this toolchain. Layout assumptions encoded in the crate-private repr module are verified to be consistent across the entire window (see docs/architecture/02-versioning-and-compatibility.md).

See docs/bump-toolchain.md for the procedure to extend the window.

Structs

SupportedToolchain

One ABI-equivalence class in the supported toolchain window.

Constants

SUPPORTED_TOOLCHAINS

The supported Lean toolchain window.

Functions

supported_by_digest

Return the SupportedToolchain entry whose header_digest matches the given lowercase-hex SHA-256 string, if any.

supported_for

Return the SupportedToolchain entry that includes version, if any.

symbol_present_in_window

Return true iff no SupportedToolchain entry lists symbol under missing_symbols. Combine with crate::REQUIRED_SYMBOLS for a membership check via crate::symbol_in_all.