From b5432d4d3b59b217282e05e4c8e59917bc3860bc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Thu, 30 Jul 2015 18:42:11 +0200 Subject: [PATCH] fix(doc): corrects language mistakes corrects two confusions between singular and plural --- doc/lean/tutorial.org | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/lean/tutorial.org b/doc/lean/tutorial.org index d6154d0306..2c32090564 100644 --- a/doc/lean/tutorial.org +++ b/doc/lean/tutorial.org @@ -630,7 +630,7 @@ tedious steps. Here is a very simple example. Lean supports _dependent functions_. In type theory, they are also called dependent product types or Pi-types. The idea is quite simple, suppose we have a type =A : Type=, and a family of types =B : A → Type= which assigns to each =a : A= a type =B a=. So a dependent function is a function whose range varies depending on its arguments. -In Lean, the dependent functions is written as =forall a : A, B a=, +In Lean, a dependent function is written as =forall a : A, B a=, =Pi a : A, B a=, =∀ x : A, B a=, or =Π x : A, B a=. We usually use =forall= and =∀= for propositions, and =Pi= and =Π= for everything else. In the previous examples, we have seen many examples of @@ -640,7 +640,7 @@ equality are all dependent functions. The universal quantifier is just a dependent function. In Lean, if we have a family of types =B : A → Prop=, then =∀ x : A, B a= has type =Prop=. -This features complicates the Lean set-theoretic model, but it +This feature complicates the Lean set-theoretic model, but it improves usability. Several theorem provers have a =forall elimination= (aka instantiation) proof rule.