From 7202e076ddb39d19e08546cfcb2005f7d5212d87 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Thu, 30 Jul 2015 18:12:13 +0200 Subject: [PATCH] fix(doc): correct language mistakes --- doc/lean/tutorial.org | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/lean/tutorial.org b/doc/lean/tutorial.org index 2993bff273..0538e59f8b 100644 --- a/doc/lean/tutorial.org +++ b/doc/lean/tutorial.org @@ -233,7 +233,7 @@ What is the type of =Type=? check Type #+END_SRC -Lean reports =Type : Type=, is it Lean inconsistent? Now, it is not. +Lean reports =Type : Type=, is Lean inconsistent? No, it is not. Internally, Lean maintains a hierarchy of Types. We say each one of them _lives_ in a universe. Lean is universe polymorphic, and by default all universes are hidden from the user. Like implicit