The Lean Language Reference
This is the Lean Language Reference, an in-progress reference work on Lean. It is intended to be a comprehensive, precise description of Lean: a reference work in which Lean users can look up detailed information, rather than a tutorial for new users. For other documentation, please refer to the Lean documentation site.