From 923d12553ed6dd01a9b3a02fbfd10f2c883ee7e7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Thu, 30 Jul 2015 18:52:56 +0200 Subject: [PATCH] fix(doc): correct two more mistakes - fix a mistake in code example - fix singular/plural confusion --- 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 d5559e3b6a..a020c15868 100644 --- a/doc/lean/tutorial.org +++ b/doc/lean/tutorial.org @@ -639,12 +639,12 @@ 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=. +then =∀ a : A, B a= has type =Prop=. This feature complicates the Lean set-theoretic model, but it improves usability. Several theorem provers have a =forall elimination= (aka instantiation) proof rule. -In Lean (and other systems based on proposition as types), this rule +In Lean (and other systems based on propositions as types), this rule is just function application. In the following example we add an axiom stating that =f x= is =0= forall =x=.