You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: Manual.lean
+14-26Lines changed: 14 additions & 26 deletions
Original file line number
Diff line number
Diff line change
@@ -32,39 +32,27 @@ set_option maxRecDepth 300000
32
32
tag := "lean-language-reference"
33
33
%%%
34
34
35
-
36
35
This is the _Lean Language Reference_, an in-progress reference work on Lean.
37
36
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 intended for new users.
38
-
For other documentation, please refer to the [Lean documentation site](https://lean-lang.org/documentation/).
39
-
40
-
This reference manual is not yet complete, but there's enough information to provide value to users.
41
-
The top priority is to add the missing information as quickly as possible while staying up to date with Lean development.
42
-
As the rest of the text is written, regular snapshots will be released, tracking upstream changes.
43
-
This snapshot covers Lean version {versionString}[].
44
-
45
-
Our prioritization of content is based on our best understanding of our users' needs.
46
-
Please use the [issue tracker](https://github.com/leanprover/reference-manual/issues) to help us better understand what you need to know.
47
-
In particular, please create or upvote issues for topics that are important to you.
48
-
Your feedback is much appreciated!
49
-
Once sufficient content is available, we will begin saving snapshots for each release of Lean and making them conveniently available.
50
-
51
-
API reference documentation is included from the Lean standard library source code.
52
-
Due to technical limitations at the moment, the Lean terms and examples embedded in it do not render as nicely as we would like.
53
-
In the near future, we will be working on removing these limitations.
54
-
Additionally, we will be adding missing API reference documentation and revising and improving the existing API reference documentation.
37
+
For other documentation, please refer to the [Lean documentation overview](https://lean-lang.org/documentation/).
38
+
This manual covers Lean version {versionString}[].
55
39
56
-
**Release History**
40
+
Lean is an *interactive theoremprover*basedondependenttypetheory,designedforusebothincutting-edgemathematicsandinsoftwareverification.
Thecoretypetheoryisimplementedinaminimal {tech}[kernel] that does nothing other than check proof terms.
43
+
This core theory and kernel are supported by advanced automation, realized in {ref "tactics"}[an expressive tactic language].
44
+
Each tactic produces a term in the core type theory that is checked by the kernel, so bugs in tactics do not threaten the soundness of Lean as a whole.
45
+
Along with many other parts of Lean, the tactic language is user-extensible, so it can be built up to meet the needs of a given formalization project.
46
+
Tactics are written in Lean itself, and can be used immediately upon definition; rebuilding the prover or loading external modules is not required.
57
47
58
-
: 2025-02-03
48
+
Lean is also a pure *functional programming language*, with features such as a run-time system based on reference counting that can efficiently work with packed array structures, multi-threading, and monadic {name}`IO`.
49
+
As befits a programming language, Lean is primarily implemented in itself, including the language server, build tool, {tech}[elaborator], and tactic system.
50
+
This very book is written in [Verso](https://github.com/leanprover/verso), a documentation authoring tool written in Lean.
59
51
60
-
This release updates the contents for Lean version 4.17.0-rc1.
61
-
It adds descriptions of {ref "well-founded-recursion"}[well-founded recursion], the new {ref "partial-fixpoint"}[partial fixpoint] feature, {ref "quotients"}[quotient types], and {ref "lake"}[Lake], and {ref "structural-recursion"}[the description of structural recursion] has been greatly improved.
62
-
Descriptions and API references for all fixed-width integer types, {name}`Int`, {name}`Fin`, {name}`Empty`, and {name}`Option` were also added.
63
-
This release also includes a quick-jump box that can be used to quickly navigate to any documented topic.
52
+
Familiarity with Lean's programming features is valuable even for users whose primary interest is in writing proofs, because Lean programs are used to implement new tactics and proof automation.
53
+
Thus, this reference manual does not draw a barrier between the two aspects, but rather describes them together so they can shed light on one another
64
54
65
-
: 2024-12-16
66
55
67
-
This is the initial release of the reference manual.
Thecoretypetheoryisimplementedinaminimal {tech}[kernel] that does nothing other than check proof terms.
40
-
This core theory and kernel are supported by advanced automation, realized in {ref "tactics"}[an expressive tactic language].
41
-
Each tactic produces a term in the core type theory that is checked by the kernel, so bugs in tactics do not threaten the soundness of Lean as a whole.
42
-
Along with many other parts of Lean, the tactic language is user-extensible, so it can be built up to meet the needs of a given formalization project.
43
-
Tactics are written in Lean itself, and can be used immediately upon definition; rebuilding the prover or loading external modules is not required.
44
-
45
-
Lean is also a pure *functional programming language*, with features such as a run-time system based on reference counting that can efficiently work with packed array structures, multi-threading, and monadic {name}`IO`.
46
-
As befits a programming language, Lean is primarily implemented in itself, including the language server, build tool, {tech}[elaborator], and tactic system.
47
-
This very book is written in [Verso](https://github.com/leanprover/verso), a documentation authoring tool written in Lean.
48
-
49
-
Familiarity with Lean's programming features is valuable even for users whose primary interest is in writing proofs, because Lean programs are used to implement new tactics and proof automation.
50
-
Thus, this reference manual does not draw a barrier between the two aspects, but rather describes them together so they can shed light on one another.
0 commit comments