2025-03-28

Since the last preview, the following content has been added:

• A chapter on Elan and its command line interface
• A description of reference counting and memory management
• Details about the specifics of unsafe and partial definitions
• A detailed description of signatures and automatic implicit parameters
• More details about reducibility
• Nested inductive types
• Axioms

The table of contents has also been reworked to better organize the information and make it easier to find.

In addition, more of the included docstrings have been edited upstream in Lean itself, and the manual is now generated with the latest nightly release of Lean.

2025-03-24

This release of the Language Reference features many revisions to the included API references. Many more functions have examples, and their style has been harmonized. The manual now includes the release notes for all versions of Lean 4.

There have been improvements to the look and feel of the rendered HTML, especially on mobile devices.

2025-03-12

This release features a visual overhaul that both improves the navigation features and makes the manual look much better. Each page now includes an overview that includes all of the documented syntax and names.

There's also plenty of new content:

• Interacting with Lean via commands such as #eval and #check
• A description of the coercions mechanism
• A description of the preprocessing mechanism for well-founded recursion that automatically introduces attach
• The remaining basic types, including but not limited to Sum, Prod,Subtype, Sigma, List, Float, BitVec, and Thunk
• Standard proposition and predicate formers, such as equality, conjunction, disjunction, implication, and quantifiers

2025-02-03r2

This release updates the contents for Lean version 4.17.0-rc1. It adds descriptions of well-founded recursion, the new partial fixpoint feature, quotient types, and Lake, and the description of structural recursion has been greatly improved. Descriptions and API references for all fixed-width integer types,Int, Fin, Empty, and Option were also added. This release also includes a quick-jump box that can be used to quickly navigate to any documented topic.

2025-02-03

This release updates the contents for Lean version 4.17.0-rc1. It adds descriptions of well-founded recursion, the new partial fixpoint feature, quotient types, and Lake, and the description of structural recursion has been greatly improved. Descriptions and API references for all fixed-width integer types,Int, Fin, Empty, and Option were also added. This release also includes a quick-jump box that can be used to quickly navigate to any documented topic.

2024-12-22

This is a quick fix for an issue with hosting. No new content.

2024-12-16r2

This fixes a last-minute HTML rendering issue in today's release, as well as a typo.

2024-12-16

This is the initial public release of the Lean Language Reference.

Public Preview 4.1

This updated preview fixes many of the mobile browser issues pointed out on Zulip. Thanks!

Public Preview 4

This preview, hopefully the final one prior to a release, greatly improves the display on mobile devices.

New content:

• Type classes
• Notations and Macros