12. 运行时代码
已编译的 Lean 代码使用 Lean 运行时提供的服务。 该运行时包含高效的低级原语，可弥合 Lean 语言和支持的平台之间的差距。 这些服务包括：
- 内存管理
Lean不需要程序员手动管理内存。 当需要存储值时会分配空间，而无法再访问（因此不相关）的值将被释放。 特别是，Lean 使用 引用计数，其中每个分配的对象都维护传入引用的计数。 编译器发出对分配内存和修改引用计数的内存管理例程的调用，这些例程由运行时提供，以及表示编译代码中的 Lean 值的数据结构。
- 多线程
TaskAPI 提供编写并行和并发代码的能力。 运行时负责跨操作系统线程调度 Lean 任务。- 原语运算符
许多内置类型（包括
Nat、Array、String和 固定位宽整数）出于效率原因具有特殊表示。 运行时提供了这些类型的原始运算符的实现，这些运算符利用了这些优化的表示形式。
有许多原始运算符。 它们在 基本类型 下各自的部分中进行了描述。