Category:Lean: Difference between revisions
Content added Content deleted
(Created page with "{{language |exec=machine |strength=strong |safety=safe |checking=both |gc=yes |LCT=yes}} {{implementation|Lean}} {{language programming paradigm|functional}} {{language progra...") |
m (added whitespace.) |
||
| Line 11: | Line 11: | ||
'''Lean'''is an open source theorem prover and programming language being developed at Microsoft Research. |
'''Lean''' is an open source theorem prover and programming language being developed at Microsoft Research. |
||
Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs. |
|||
https://leanprover.github.io/about/ |
https://leanprover.github.io/about/ |
||
Latest revision as of 19:22, 17 July 2020
This programming language may be used to instruct a computer to perform a task.
| Execution method: | Compiled (machine code) |
|---|---|
| Garbage collected: | Yes |
| Type safety: | Safe |
| Type strength: | Strong |
| Type checking: | Dynamic, Static |
| See Also: |
Lean is an implementation of Lean.
Other implementations of Lean.
Lean is an open source theorem prover and programming language being developed at Microsoft Research.
Lean aims to bridge the gap between interactive and automated theorem proving, by situating automated tools and methods in a framework that supports user interaction and the construction of fully specified axiomatic proofs.
Pages in category "Lean"
The following 7 pages are in this category, out of 7 total.