Skip to content

various changes to the docs #149

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
oxe-i merged 2 commits into from
Feb 22, 2026
Merged

various changes to the docs #149

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a19c803
various changes to the docs
Feb 22, 2026
3f7cf01
insert spaces at the start of the line in RESOURCES.md
Feb 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 1 addition & 11 deletions docs/INSTALLATION.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion docs/LEARNING.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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/
Expand Down
2 changes: 2 additions & 0 deletions docs/RESOURCES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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/
12 changes: 7 additions & 5 deletions docs/TESTS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading