Commit graph

3 commits

Author SHA1 Message Date
Marc Huisinga
f220efc5ba
doc: update quickstart guide for new display name (#5193)
https://github.com/leanprover/vscode-lean4/pull/521 changed the display
name of the VS Code extension so that it can be found more easily when
searching for "Lean" (before it would appear far down in the list). This
PR updates the quickstart guide to reflect this fact.
2024-08-28 13:29:16 +00:00
Marc Huisinga
b2ee8c240d
doc: update quickstart guide (#4806)
This PR updates the screenshots and instructions in the quickstart guide
for the most recent Lean 4 VS Code extension version and makes a small
stylistic change suggested by @semorrison.
2024-07-23 07:31:21 +00:00
Sebastian Ullrich
dcfd6f4873 doc: quickstart 2021-04-06 17:34:01 +02:00