20. Run-Time Code🔗

Compiled Lean code uses services provided by the Lean runtime. The runtime contains efficient, low-level primitives that bridge the gap between the Lean language and the supported platforms. These services include:

Memory management: Lean does not require programmers to manually manage memory. Space is allocated when needed to store a value, and values that can no longer be reached (and are thus irrelevant) are deallocated. In particular, Lean uses reference counting, where each allocated object maintains a count of incoming references. The compiler emits calls to memory management routines that allocate memory and modify reference counts, and these routines are provided by the runtime, along with the data structures that represent Lean values in compiled code.
Multiple Threads: The Task API provides the ability to write parallel and concurrent code. The runtime is responsible for scheduling Lean tasks across operating-system threads.
Primitive operators: Many built-in types, including Nat, Array, String, and fixed-width integers, have special representations for reasons of efficiency. The runtime provides implementations of these types' primitive operators that take advantage of these optimized representations.

There are many primitive operators. They are described in their respective sections under Basic Types.