michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(doc): corrects language mistakes

Browse source 
corrects two confusions between singular and plural
This commit is contained in:
Théo Zimmermann 2015-07-30 18:42:11 +02:00 committed by Leonardo de Moura
parent c4e48a184c
commit b5432d4d3b
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/lean/tutorial.org
View file

@ -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.