This document is the primary reference for the Lean
It focuses on providing:
- Informal explanations of the language and its use.
- A formal presentation of Lean's meta theory and axioms.
- A description of the languages runtime, async proof checking ...
This document is not intended to be an
introduction to the language.
We provide separate books intended to for most users of Lean, one focused on
theorem proving and
another on programming with Lean.
This document only covers the minimal library details needed by Lean,
the standard library is documented separately, with the hope of using
leandoc to extract and host documentation elsewhere in the future.