From 8375626cb697640ce91c8d24568be334f739ecf7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Aug 2014 18:32:53 -0700 Subject: [PATCH] fix(doc/lean/tutorial): adjust tutorial to library changes, fix test Signed-off-by: Leonardo de Moura --- doc/lean/tutorial.org | 5 ++--- tests/lean/empty.lean.expected.out | 4 ++-- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/doc/lean/tutorial.org b/doc/lean/tutorial.org index 32bd2531b..f1cca3b93 100644 --- a/doc/lean/tutorial.org +++ b/doc/lean/tutorial.org @@ -761,7 +761,7 @@ of two even numbers is an even number. exists_intro (w1 + w2) (calc a + b = 2*w1 + b : {Hw1} ... = 2*w1 + 2*w2 : {Hw2} - ... = 2*(w1 + w2) : symm (mul_add_distr_right 2 w1 w2)))) + ... = 2*(w1 + w2) : symm (mul_distr_left 2 w1 w2)))) #+END_SRC @@ -781,6 +781,5 @@ With this macro we can write the example above in a more natural way exists_intro (w1 + w2) (calc a + b = 2*w1 + b : {Hw1} ... = 2*w1 + 2*w2 : {Hw2} - ... = 2*(w1 + w2) : symm (mul_add_distr_right 2 w1 w2)) + ... = 2*(w1 + w2) : symm (mul_distr_left 2 w1 w2)) #+END_SRC - diff --git a/tests/lean/empty.lean.expected.out b/tests/lean/empty.lean.expected.out index e13eabedf..88c2487e3 100644 --- a/tests/lean/empty.lean.expected.out +++ b/tests/lean/empty.lean.expected.out @@ -1,5 +1,5 @@ -empty.lean:5:25: error: type error in placeholder assigned to - inhabited_Prop +empty.lean:6:25: error: type error in placeholder assigned to + Prop_inhabited placeholder has type inhabited Prop but is expected to have type