Documentation

• 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