Skip to content

v0.0.120

Choose a tag to compare

View all tags
@github-actions github-actions released this 27 Nov 10:57
· 449 commits to master since this release
v0.0.120
61b60a5
  • Update the setup guide to be more detailed and include information on VS Code extension features that do not immediately present themselves to users
  • Build standalone Lean projects after initialization so that users do not get an "imports outdated" error immediately after
  • Change scope ID of Lean's markdown grammar so that it doesn't conflict with that of the Lean 3 extension
  • Add \rrbracket to list of abbreviations
Assets 3
Loading