Documentation

• A Tour of LeanThe best way to learn about Lean is to read and write Lean code. This article will act as a tour through some of the key features of the Lean language and give you some code snippets that you can...Read more
• Semantic HighlightingThe Lean language server provides semantic highlighting information to editors. In order to benefit from this in VSCode, you may need to activate the "Editor > Semantic Highlighting" option in the...Read more
• Syntax Highlighting Lean in LaTeXYou can copy highlighted code straight from VS Code to any rich text editor supporting HTML input. For highlighting code in LaTeX, there are two options:listings, which is a common package and simple...Read more