Skip to content

Commit

Permalink
fix(01,README): Lean2 -> Lean 2
Browse files Browse the repository at this point in the history
  • Loading branch information
avigad committed Jan 31, 2017
1 parent f9fb0c7 commit d0dd6d0
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion 01_Introduction.org
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion README.md
Expand Up @@ -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
------------
Expand Down

0 comments on commit d0dd6d0

Please sign in to comment.