From 698b368f0105a8e58b0bc403d66e624bdc6699e7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Thu, 30 Jul 2015 19:00:26 +0200 Subject: [PATCH] fix(doc): fix confusion between Prop and Bool 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 --- 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 a020c15868..dda96b670a 100644 --- a/doc/lean/tutorial.org +++ b/doc/lean/tutorial.org @@ -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 -=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=. 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.