Skip to main content

Module consts

Module consts 

Source
Expand description

Compile-time constants resolved by build.rs (version + header digest) plus the tag enum from lean.h:83–95.

Constants§

LEAN_ARRAY
LEAN_CLOSURE
LEAN_CLOSURE_MAX_ARGS
LEAN_EXTERNAL
LEAN_HEADER_DIGEST
SHA-256 of the resolved lean.h. Computed by build.rs and equal to the header_digest of the matched SupportedToolchain entry.
LEAN_HEADER_PATH
Filesystem path to the lean.h that the build was resolved against.
LEAN_MAX_CTOR_FIELDS
LEAN_MAX_CTOR_SCALARS_SIZE
LEAN_MAX_CTOR_TAG
LEAN_MAX_SMALL_OBJECT_SIZE
LEAN_MPZ
LEAN_OBJECT_SIZE_DELTA
LEAN_PROMISE
LEAN_REF
LEAN_RESERVED
LEAN_RESOLVED_VERSION
Version string from the matched supported-toolchain entry.
LEAN_SCALAR_ARRAY
LEAN_STRING
LEAN_STRUCT_ARRAY
LEAN_TASK
LEAN_THUNK
LEAN_VERSION
LEAN_VERSION_STRING as read from the active toolchain’s version.h (e.g. "4.29.1").