Crate lean_rs_interop_shims 

Package-owned Lean source payload for the generic lean-rs interop shims.

Downstream build scripts use this crate when they need a Lake dependency on LeanRsInterop without assuming a sibling lean-rs checkout. The helper copies only the Lean/C payload into a caller-owned root and writes a generated lean-toolchain for the downstream toolchain.

Structs

LeanRsInteropShimsSourcePackage

Materialized interop shim source package.

LeanRsInteropShimsSourcePackageRequest

Request to materialize the packaged interop shim source for one toolchain.

Constants

LIBRARY_NAME

Lean library/root module name for the generic interop shims.

PACKAGE_NAME

Lake package name for the generic interop shims.

Functions

materialize_source_package

Materialize the packaged interop shim source package.