12. 运行时代码🔗

编译后的 Lean 代码会使用 Lean 运行时提供的服务。运行时包含高效的底层原语，用于衔接 Lean 语言与其支持的平台。这些服务包括：

内存管理: Lean 不要求程序员手动管理内存。系统会在需要存储值时分配空间，并释放那些已无法访问（因而也不再有用）的值。具体来说，Lean 使用引用计数，每个已分配对象都会维护指向它的引用数量。编译器会生成对内存管理例程的调用，用以分配内存和修改引用计数；这些例程由运行时提供，编译后代码中用于表示 Lean 值的数据结构也是如此。
多线程: Task API 可用于编写并行及并发代码。运行时负责在操作系统线程间调度 Lean 任务。
原语运算符: 出于效率考虑，许多内置类型都有特殊的表示方式，包括 Nat、Array、String 和定宽整数。运行时为这些类型实现原语运算符，以利用这些优化过的表示方式。

原语运算符有很多。各运算符的说明见基本类型下相应的小节。