diff --git a/01_Introduction.org b/01_Introduction.org index f4f026ba..4c69c508 100644 --- a/01_Introduction.org +++ b/01_Introduction.org @@ -4,7 +4,7 @@ * Introduction #+begin_warning -Please note that this is the tutorial for [[https://github.com/leanprover/lean2][Lean2]], which allows the use of +Please note that this is the tutorial for [[https://github.com/leanprover/lean2][Lean 2]], which allows the use of homotopy type theory (HoTT). It is /not/ the [[https://leanprover.github.io/introduction_to_lean][tutorial]] for the [[https://github.com/leanprover/lean][current version of Lean]]. #+end_warning diff --git a/README.md b/README.md index 50d7793e..0b90c47e 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,7 @@ Lean Tutorial - Web : https://leanprover.github.io/tutorial - PDF : https://leanprover.github.io/tutorial/tutorial.pdf -Please note that this is the tutorial for [Lean2](https://github.com/leanprover/lean2), which allows the use of homotopy type theory (HoTT). It is /not/ the [tutorial](https://leanprover.github.io/introduction_to_lean) for the [current version of Lean](https://github.com/leanprover/lean). +Please note that this is the tutorial for [Lean 2](https://github.com/leanprover/lean2), which allows the use of homotopy type theory (HoTT). It is /not/ the [tutorial](https://leanprover.github.io/introduction_to_lean) for the [current version of Lean](https://github.com/leanprover/lean). How to Build ------------