message: doc: code review feedback.
diff: @@ -5,8 +5,8 @@ It is based on [vscode-lean](https://github.com/leanprover/vscode-lean).
  ## Installing the extension and Lean 4
  1. Install the extension from the [marketplace](https://marketplace.visualstudio.com/items?itemName=leanprover.lean4).
  -1. Open a folder containing .lean code using VS Code. It is recommended that you open a folder that is configured using [lake](https://github.com/leanprover/lake) which is a lean package configuration tool.
  -1. Open a `.lean` file and type in `#eval 1`. The extension should display a blue underline below `#eval`. Upon hovering over it, a hover panel reporting the result of the evaluation should pop up. When hovering over the `1`, a hover panel displaying the type of `1` should pop up.
  +1. Open a folder containing Lean code (files with the `.lean` extension) using VS Code. It is recommended that you open a folder that is configured using [lake](https://github.com/leanprover/lake) which is a lean package configuration tool.
  +1. Open a Lean source file and type in `#eval 1`. The extension should display a blue underline below `#eval`. Upon hovering over it, a hover panel reporting the result of the evaluation should pop up. When hovering over the `1`, a hover panel displaying the type of `1` should pop up saying `1 : Nat` meaning 1 is a Natural number.
  1. If `Lean` is not yet installed on your system you will see a prompt like this:
  ![prompt](vscode-lean4/media/install-elan.png)
  1. Click the "Install Lean using Elan" option and enter any options that appear
  