Introducing the Lean Language Reference

The new Lean reference manual is officially released, just in time for your holiday projects!

The reference manual will be a comprehensive, concise, and accurate description of Lean. Even though it’s not yet totally comprehensive, it does contain descriptions of the tactic language, the most important parts of the term language, inductive datatypes and structures, and details about the elaboration process. Built using the documentation authoring DSL Verso, the reference manual includes tests that help us keep it up to date as Lean improves.

In the coming months, we will be adding new content, prioritized according to our best understanding of Lean’s users’ needs. You can best influence that understanding by creating or upvoting issues in the source repository. Issues for particular documentation topics are also a great place to describe the specifics of what you need to know so we can ensure that the result is as useful as possible.

There’s a few technical caveats with this first release:

• The included API references are Lean docstrings. We will go through them to harmonize their language use and structure and better integrate them with the reference manual, but we have not yet done so.

• Lean code in docstrings is not yet reliably syntax-highlighted or elaborated. This will improve.

• There’s no built-in search. This is already under development.

In the immediate future, the manual will track Lean development closely. Once we believe that it’s comprehensive enough for this to make sense, we’ll begin making release-specific snapshots, but for now we plan to use our resources on improving content.

The Lean community on Zulip deserves a big thanks for their feedback on early preview releases of the reference manual. Their feedback led to many improvements to the navigation and user interface. If you encounter difficulties, please open an issue so we can improve it!