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

fix(doc): fix confusion between Prop and Bool

Browse source 
this fix assumes that Prop and Bool are two different things but even if they were the same thing, using the two names would only confuse the reader
This commit is contained in:
Théo Zimmermann 2015-07-30 19:00:26 +02:00 committed by Leonardo de Moura
parent 923d12553e
commit 698b368f01
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/lean/tutorial.org
View file

@ -709,7 +709,7 @@ for =∃ a : nat, a = w= using
Note that =exists.intro= also has implicit arguments. For example, Lean has to infer the implicit argument Note that =exists.intro= also has implicit arguments. For example, Lean has to infer the implicit argument
=P : A → Bool=, a predicate (aka function to Prop). This creates complications. For example, suppose =P : A → Prop=, a predicate (aka function to Prop). This creates complications. For example, suppose
we have =Hg : g 0 0 = 0= and we invoke =exists.intro 0 Hg=. There are different possible values for =P=. we have =Hg : g 0 0 = 0= and we invoke =exists.intro 0 Hg=. There are different possible values for =P=.
Each possible value corresponds to a different theorem: =∃ x, g x x = x=, =∃ x, g x x = 0=, Each possible value corresponds to a different theorem: =∃ x, g x x = x=, =∃ x, g x x = 0=,
=∃ x, g x 0 = x=, etc. Lean uses the context where =exists.intro= occurs to infer the users intent. =∃ x, g x 0 = x=, etc. Lean uses the context where =exists.intro= occurs to infer the users intent.