From 800d3bd70a475e8f8184ad292766172cc85cb3fa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 Aug 2014 11:22:15 -0700 Subject: [PATCH] fix(doc/lean/tutorial): typos Signed-off-by: Leonardo de Moura --- 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 f1cca3b933..d8029a8075 100644 --- a/doc/lean/tutorial.org +++ b/doc/lean/tutorial.org @@ -441,7 +441,7 @@ Lean. The theorems can be broken into three different categories: introduction, elimination, and rewriting. First, we cover the introduction and elimination theorems for the basic Boolean connectives. -*** And (conjuction) +*** And (conjunction) The expression =and_intro H1 H2= creates a proof for =a ∧ b= using proofs =H1 : a= and =H2 : b=. We say =and_intro= is the _and-introduction_ operation. @@ -477,7 +477,7 @@ Now, we prove =p ∧ q → q ∧ p= with the following simple proof term. Note that the proof term is very similar to a function that just swaps the elements of a pair. -*** (disjuction) +*** (disjunction) The expression =or_intro_left b H1= creates a proof for =a ∨ b= using a proof =H1 : a=. Similarly, =or_intro_right a H2= creates a proof for =a ∨ b= using a proof =H2 : b=.