24. Lean as a Library
Lean is a self-hosted language, in the sense that most of its implementation (parser, elaborator, compiler, the metaprogramming framework) is written in Lean itself.
These components are accessed by importing modules from the Lean library.
Parts of the Lean library may also be useful for more general programming applications.
Note that the library is evolving quickly, and does not necessarily enjoy the same level of polish or stability guarantees as the standard library Std.
Furthermore, it is a large library, and importing it outside the metaprogramming phase may substantially increase the size of compiled executables.