Module memory 

Runtime memory guardrail entry points.

These symbols are exported by libleanshared but are not part of lean.h’s object ABI. They configure Lean’s best-effort memory checks; they do not reclaim retained runtime state.

Functions

lean_internal_set_max_memory^⚠

Set Lean’s process-global maximum memory in bytes.