doc: add more information to walkthrough (leanprover#362)

vscode-lean4/media/guide-documentation.md

@@ -20,7 +20,13 @@ If you want to dive right into using Lean 4 to prove elementary theorems about n
 [Lean's website](https://lean-lang.org/) links to learning resources, publications, talks and articles about Lean.
 
 **Lean Community**  
-The [Lean Community website](https://leanprover-community.github.io/index.html) links to several other helpful learning resources not listed here and provides an introduction to [mathlib](https://github.com/leanprover-community/mathlib4), Lean's math library.
+The [Lean Community website](https://leanprover-community.github.io/index.html) links to several other helpful learning resources not listed here and provides an introduction to [Mathlib](https://github.com/leanprover-community/mathlib4), Lean's math library.
 
 **Manual**  
 The [Lean Manual](https://lean-lang.org/lean4/doc/) documents several features of Lean 4 and can be consulted for some of the more technical details concerning Lean.
+
+## Finding Definitions and Theorems
+There are two search engines that help you find definitions and theorems in [Mathlib](https://github.com/leanprover-community/mathlib4), [Lean's standard library](https://github.com/leanprover/std4) and Lean 4 itself:
+
+- [Loogle](https://loogle.lean-lang.org/): A pattern-based search engine that finds definitions and theorems by type signature or by the names of their identifiers.
+- [Moogle](https://www.moogle.ai/): An AI-based search engine that finds definitions and theorems by a description in natural language.

vscode-lean4/media/guide-help.md

@@ -1,6 +1,12 @@
+## Collecting VS Code Output
+If you are encountering an issue with this VS Code extension, copying the output from the 'Lean: Editor' output panel can be helpful for others who are trying to help you. 
+You can open the 'Lean: Editor' output panel by clicking on the ∀-symbol in the top right and selecting 'Troubleshooting: Show Output'.
+
+  ![Show Output](show-output.png)
+
 ## Asking Questions on the Lean Zulip Chat
 
-To post your question on the [Lean Zulip chat](https://leanprover.zulipchat.com/), you can follow these steps:
+To post a question on the [Lean Zulip chat](https://leanprover.zulipchat.com/), you can follow these steps:
 1. [Create a new Lean Zulip chat account](https://leanprover.zulipchat.com/register/).
 2. [Visit the #new-members stream](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members).
 3. Click the 'New topic' button at the bottom of the page, enter a topic title, describe your question or issue in the message text box and click 'Send'.

vscode-lean4/media/guide-installDeps-linux.md

@@ -15,4 +15,4 @@
 ## Restricted Environments
 If you are in an environment where you cannot install Git or curl, for example a restricted university computer, you can check if you already have them installed by [opening a new terminal](command:workbench.action.terminal.new), typing in `which git curl` and pressing Enter. If the terminal output displays two file paths and no error, you already have them installed.  
 
-If your machine does not already have Git and curl installed and you cannot install them, there is currently no option to try Lean 4 with a local installation. If you want to try out Lean 4 regardless, you can read [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) and do the exercises with [an online instance of Lean 4 hosted using Gitpod](https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean). Doing so requires creating a GitHub account.
+If your machine does not already have Git and curl installed and you cannot install them, there is currently no option to try Lean 4 with a local installation. If you want to try out Lean 4 regardless, you can read [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) and do the exercises with [an online instance of Lean 4 hosted using Gitpod](https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean). Doing so requires creating a GitHub account. Alternatively, you can also [play the Natural Number Game](https://adam.math.hhu.de/#/g/hhu-adam/NNG4) or [try a single-file version of Lean 4 in your web browser](https://live.lean-lang.org/).

vscode-lean4/media/guide-installDeps-mac.md

@@ -13,4 +13,4 @@
 ## Restricted Environments
 If you are in an environment where you cannot install Homebrew, Git or curl, for example a restricted university computer, you can check if you already have them installed by [opening a new terminal](command:workbench.action.terminal.new), typing in `which git curl` and pressing Enter. If the terminal output displays two file paths and no error, you already have them installed.  
 
-If your machine does not already have Homebrew, Git and curl installed and you cannot install them, there is currently no option to try Lean 4 with a local installation. If you want to try out Lean 4 regardless, you can read [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) and do the exercises with [an online instance of Lean 4 hosted using Gitpod](https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean). Doing so requires creating a GitHub account.
+If your machine does not already have Homebrew, Git and curl installed and you cannot install them, there is currently no option to try Lean 4 with a local installation. If you want to try out Lean 4 regardless, you can read [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) and do the exercises with [an online instance of Lean 4 hosted using Gitpod](https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean). Doing so requires creating a GitHub account. Alternatively, you can also [play the Natural Number Game](https://adam.math.hhu.de/#/g/hhu-adam/NNG4) or [try a single-file version of Lean 4 in your web browser](https://live.lean-lang.org/).

vscode-lean4/media/guide-installDeps-windows.md

@@ -6,4 +6,4 @@
 [Git](https://git-scm.com/) is a commonly used [Version Control System](https://en.wikipedia.org/wiki/Version_control) that is used by Lean to help manage different versions of Lean formalization packages and software packages.
 
 ## Restricted Environments
-If you are in an environment where you cannot install Git and it is not already installed, for example on a restricted university computer, there is currently no option to try Lean 4 with a local installation. If you want to try out Lean 4 regardless, you can read [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) and do the exercises with [an online instance of Lean 4 hosted using Gitpod](https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean). Doing so requires creating a GitHub account.
+If you are in an environment where you cannot install Git and it is not already installed, for example on a restricted university computer, there is currently no option to try Lean 4 with a local installation. If you want to try out Lean 4 regardless, you can read [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) and do the exercises with [an online instance of Lean 4 hosted using Gitpod](https://gitpod.io/#/https://github.com/leanprover-community/mathematics_in_lean). Doing so requires creating a GitHub account. Alternatively, you can also [play the Natural Number Game](https://adam.math.hhu.de/#/g/hhu-adam/NNG4) or [try a single-file version of Lean 4 in your web browser](https://live.lean-lang.org/).

vscode-lean4/media/guide-installElan-unix.md

@@ -2,3 +2,5 @@
 [Elan](https://github.com/leanprover/elan) automatically manages all the different versions of Lean and ensures that the correct version is used when opening a project.
 
 Clicking [this link](command:lean4.setup.installElan) will download the [Elan setup script](https://github.com/leanprover/elan/blob/master/elan-init.sh) and execute it.
+
+If the script executes without displaying an error, both Elan and a current stable version of Lean 4 have been installed. If it displays an error that you do not understand, click on the 'Questions and Troubleshooting' step on the left.

vscode-lean4/media/guide-installElan-windows.md

@@ -2,3 +2,5 @@
 [Elan](https://github.com/leanprover/elan) automatically manages all the different versions of Lean and ensures that the correct version is used when opening a project.
 
 Clicking [this link](command:lean4.setup.installElan) will download the [Elan setup script](https://github.com/leanprover/elan/blob/master/elan-init.ps1) and execute it.
+
+If the script executes without displaying an error, both Elan and a current stable version of Lean 4 have been installed. If it displays an error that you do not understand, click on the 'Questions and Troubleshooting' step on the left.

vscode-lean4/media/guide-setupProject.md

@@ -1,15 +1,22 @@
-## Project Creation
+## Creating a Project
+Below, you will find links that create new projects or download projects for you. After creating or downloading a project, you can re-open the project in the future by clicking the ∀-symbol in the top right, choosing 'Open Project…' > 'Open Local Project…' and selecting the project you created.  
+Completing the project creation process and choosing to open the new project will close this guide. You can re-open it later by clicking the ∀-symbol in the top right and selecting 'Documentation…' > 'Setup: Show Setup Guide'.
+
+  ![∀-symbol buttons](open-local-project_show-setup_buttons.png)
+
 If you want to create a new project, click on one of the following:
 - [Create a new standalone project](command:lean4.project.createStandaloneProject)  
-  Standalone projects do not depend on any other Lean 4 projects. Dependencies can be added by modifying 'lakefile.lean' in the newly created project as described [here](https://github.com/leanprover/lean4/blob/master/src/lake/README.md#adding-dependencies).
+  Standalone projects do not depend on any other Lean 4 projects. This option is suitable if you want to use Lean 4 as a general-purpose programming language or for program verification.  
+  Dependencies can be added by modifying 'lakefile.lean' in the newly created project as described [here](https://github.com/leanprover/lean4/blob/master/src/lake/README.md#adding-dependencies). You may want to add [Lean's standard library](https://github.com/leanprover/std4) to the list of dependencies.
 - [Create a new project using Mathlib](command:lean4.project.createMathlibProject)  
-  The created project will depend on [Mathlib](https://github.com/leanprover-community/mathlib4), the math library of Lean 4.
+  The created project will depend on [Mathlib](https://github.com/leanprover-community/mathlib4), the math library of Lean 4. This option is suitable if you want to use Lean 4 for a math formalization project.  
+  To update Mathlib after creating the project, you can click the ∀-symbol in the top right and choose 'Project Actions…' > 'Project: Update Dependency…'.
 
 If you want to open an existing project, click on one of the following:
-- [Download an existing project](command:lean4.project.clone)
-- [Open an existing local project](command:lean4.project.open)
-
-After creating or downloading a project, you can open it in the future by clicking the ∀-symbol in the top right, choosing 'Open Project…' > 'Open Local Project…' and selecting the project you created.
+- [Download an existing project](command:lean4.project.clone)  
+  This option is suitable if you want to contribute to another Lean 4 project, like [Mathlib](https://github.com/leanprover-community/mathlib4).
+- [Open an existing local project](command:lean4.project.open)  
+  This option is suitable if you have been provided with a local Lean 4 project by someone else, like an instructor.
 
 ## Complex Project Setups
 Using its build system and package manager Lake, Lean 4 supports more complex project setups than the ones described above. You can find out more about Lake in the [Lean 4 GitHub repository](https://github.com/leanprover/lean4/blob/master/src/lake/README.md).

vscode-lean4/media/guide-vscode.md

@@ -0,0 +1,30 @@
+## Using Lean 4 in VS Code
+
+**Working with multiple files**  
+When working on a Lean 4 file `A.lean` that imports another Lean 4 file `B.lean`, you will notice that changes to `B.lean` do not automatically appear in `A.lean`.
+To make them appear, select the tab for `A.lean`, click on the ∀-symbol in the top right and select 'Server: Restart File' (Ctrl+Shift+X).
+This manual interaction helps to prevent accidental and potentially expensive rebuilds of the project.
+
+  ![Restart File](restart-file.png)
+
+**Inputting Unicode Symbols**  
+You can input Unicode symbols in Lean 4 files by typing a backslash (`\`) character followed by the name of the Unicode symbol.
+For example, `\all` becomes `∀` and `\Nat` becomes `ℕ`.
+
+If you encounter a Unicode symbol in Lean 4 code and want to learn how to type it, you can hover over the symbol with your mouse and it will display the name of the Unicode symbol.
+
+  ![Unicode Hover](unicode-hover.png)
+
+A full list of all Unicode symbol names can be found by clicking on the ∀-symbol in the top right and selecting 'Documentation…' > 'Docview: Show All Abbreviations'.
+
+**Navigating Lean 4 Code**  
+Right-clicking on any identifer will bring up the following context menu:
+
+  ![Context Menu](context-menu.png)
+
+The two most important entries in this list are 'Go to Definition' and 'Find All References'.  
+'Go to Definition' will take you to the file that defines the identifier, whereas 'Find All References' will display all locations where the identifier is used.
+
+If you know the name of an identifier but are not sure where to find it, you can open the symbol search by hitting 'Ctrl+P' and typing in `#` followed by the name of the identifier. The search will bring up all identifiers containing the given name and clicking on any of the results will take you to the file where it is defined.
+
+  ![Symbol Search](symbol-search.png)