various changes to the docs (exercism#149)

Author: oxe-i

docs/INSTALLATION.md

@@ -2,14 +2,4 @@
 
 You can install Lean by following the [installation instructions][install] on the official website.
 
-The recommended way to install Lean is through **Visual Studio Code** and the **Lean 4 VS Code** extension.
-This extension automatically installs all required dependencies.
-It also includes syntax highlighting, code completion, version management, links to learning resources and documentation, and many other useful tools.
-
-There are also alternative methods for [manual installation][manual-install], with support for some other editors.
-
-You can also try out the language on the official [web playground][playground] without installing anything.
-
-[install]: https://lean-lang.org/install/
-[manual-install]: https://lean-lang.org/install/manual/
-[playground]: https://live.lean-lang.org/
+[install]: https://lean-lang.org/instal

docs/LEARNING.md

@@ -10,7 +10,7 @@ For a more in-depth look at theorem proving in Lean, the book [Theorem Proving i
 
 [The Lean Language Reference][lean-reference] is the authoritative source for detailed information about the language.
 
-Many additional resources for learning Lean are made available by the community in [this repository][community-resources].
+Many additional resources for learning Lean are made available by the [Lean Community][community-resources].
 
 [community-resources]: https://leanprover-community.github.io/learn.html
 [functional-programming]: https://lean-lang.org/functional_programming_in_lean/

docs/RESOURCES.md

@@ -1,13 +1,15 @@
 # Resources
 
 * The [official site][lean-lang] is the main repository for content about the language.
+  It has an online [playground][playground] where you can try out the language without installing anything.
 * The [Reservoir][reservoir] indexes, builds and tests packages within the Lean and Lake ecosystem.
   It is the place to go for third-party packages.
 * [Lean Community][community] is a collaborative, open-source network around the Lean ecosystem.
   It is responsible for _mathlib_, the main community-driven mathematics library for Lean 4.
 * [Lean 4 Zulip Chat][zulip-chat] is the main chat for the Lean Community.
 
 [lean-lang]: https://lean-lang.org/
+[playground]: https://live.lean-lang.org/
 [reservoir]: https://reservoir.lean-lang.org/
 [community]: https://leanprover-community.github.io/index.html
 [zulip-chat]: https://leanprover.zulipchat.com/

docs/TESTS.md

@@ -51,25 +51,27 @@ All of them are expected to be defined in the solution module, within a namespac
 Each argument and the return value for each function has some type.
 This might be one of the basic types in Lean (for example, `Nat`, `List Int` or `Option String`), or a user-defined type.
 
-You'll a find a file with the correct name already in place in the same folder as the test module.
+You will find a file with the correct name already in place in the same folder as the test module.
 This file should have a _stub_ with most initial informations, so that you can use it as a starting point for your solution.
 
 Just keep in mind that this stub is there just for you to get started. 
 Feel free to change it completely if you think it is the right thing to do.
 
 ## Using packages
 
-Lean projects using Lake may always import the standard library `Std`, which contains additional data structures, IO and system APIs, and other basic utilities.
-This import should be at the beggining of the file:
+Lean projects using Lake may always import the standard library `Std`, which contains additional data structures, I/O and system APIs, and other basic utilities.
+This import should be at the beginning of the file:
 
 ```lean
 import Std
 
 def someMap : Std.HashMap Int Nat := ...
 ```
 
-Note that the module name is its namespace, so in this example the type `HashMap` was qualified with `Std`, the package where it is defined.
-It is possible to open a module, so that all its data structures and functions are available without this namespace qualification:
+In this example, the type `HashMap` is qualified with `Std`, the namespace where it is defined.
+All resources in the standard library are in the same namespace, `Std`.
+
+It is also possible to open a module so that all its data structures and functions are available without this namespace qualification:
 
 ```lean
 import Std