max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: fix mathlib link in README

Browse source
This commit is contained in:
tydeu 2021-11-21 16:55:29 -05:00
parent 8a1e413d5a
commit bb2c720411
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
README.md
View file

@ -5,7 +5,7 @@ With Lake, package configuration is written in Lean inside a dedicated `lakefile
## Getting Lake
Lake is part of the [`lean4`](https://github.com/leanprover/lean4) repository and is distributed along with its official releases (e.g., as part of the [`elan`](https://github.com/leanprover/elan) toolchain). So if you have installed a semi-recent Lean 4 nightly, you should already have it!
Lake is part of the [lean4](https://github.com/leanprover/lean4) repository and is distributed along with its official releases (e.g., as part of the [elan](https://github.com/leanprover/elan) toolchain). So if you have installed a semi-recent Lean 4 nightly, you should already have it!
Note that the Lake included with Lean is not updated as frequently as this repository, so some bleeding edge features may be missing. If you want to build the latest version from the source yourself, check out the build instructions at the bottom of this README.
@ -67,7 +67,7 @@ Hello, world!
Lake packages can also have dependencies. Dependencies are other Lake packages the current package needs in order to function. To define a dependency, add an entry to the `dependencies` field of the package configuration. Each entry includes the name of the package and where to find it. Dependencies can be sourced directly from a local folder (e.g., a subdirectory of the package) or come from remote Git repositions.
For example, one can depend on the Lean 4 port of [`mathlib`]() like so:
For example, one can depend on the Lean 4 port of [mathlib](https://github.com/leanprover-community/mathlib4) like so:
```lean
package hello {