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

doc: fix heading

Browse source
This commit is contained in:
tydeu 2022-06-09 20:57:20 -04:00
parent 1f017deaa0
commit 6f38ebebe9
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

@ -14,7 +14,7 @@ With Lake, package configuration is written in Lean inside a dedicated `lakefile
+ [Lean Libraries](#lean-libraries)
+ [Binary Executables](#binary-executables)
* [Adding Dependencies](#adding-dependencies)
+ [Syntax of `Require`](#syntax-of-require)
+ [Syntax of `require`](#syntax-of-require)
* [Writing and Running Lake Scripts](#writing-and-running-lake-scripts)
* [Building and Running Lake from the Source](#building-and-running-lake-from-the-source)
+ [Building with Nix Flakes](#building-with-nix-flakes)
@ -174,7 +174,7 @@ require mathlib from git
The next run of `lake build` (or refreshing dependencies in an editor like VSCode) will clone the mathlib repository and build it. Information on the specific revision cloned will then be saved to `manifest.json` in the workspace's `packageDir` (by default, `lean_packages`) to enable reproducibility. To update `mathlib` after this, you will need to run `lake update` -- other commands do not update resolved dependencies.
### Syntax of `Require`
### Syntax of `require`
The `require` command has two forms: