From 589f9df1032c20b493b0407ed8e245f801093384 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 13 Jul 2015 21:46:09 -0400
Subject: [PATCH] fix(tests/lean): adjust tests to reflect recent changes in
 the standard library

---
 .../lean/interactive/findp.input.expected.out |  4 ++++
 tests/lean/rw_set2.lean.expected.out          | 17 ++++++++++++++++
 tests/lean/rw_set3.lean.expected.out          | 20 +++++++++++++++++++
 3 files changed, 41 insertions(+)

diff --git a/tests/lean/interactive/findp.input.expected.out b/tests/lean/interactive/findp.input.expected.out
index 1216c8626..e9a219f54 100644
--- a/tests/lean/interactive/findp.input.expected.out
+++ b/tests/lean/interactive/findp.input.expected.out
@@ -8,15 +8,19 @@ false.rec_on|Π (C : Type), false → C
 false.cases_on|Π (C : Type), false → C
 false.induction_on|∀ (C : Prop), false → C
 true_ne_false|¬true = false
+nat.lt_self_iff_false|∀ (n : nat), nat.lt n n ↔ false
 not_of_is_false|is_false ?c → ¬?c
 not_of_iff_false|(?a ↔ false) → ¬?a
 p_ne_false|?p → ?p ≠ false
 is_false|Π (c : Prop) [H : decidable c], Prop
+nat.lt_zero_iff_false|∀ (a : nat), nat.lt a nat.zero ↔ false
 not_of_eq_false|?p = false → ¬?p
+nat.succ_le_self_iff_false|∀ (n : nat), nat.le (nat.succ n) n ↔ false
 decidable.rec_on_false|Π (H3 : ¬?p), ?H2 H3 → decidable.rec_on ?H ?H1 ?H2
 not_false|¬false
 decidable_false|decidable false
 of_not_is_false|¬is_false ?c → ?c
 iff_false_intro|¬?a → (?a ↔ false)
+nat.succ_le_zero_iff_false|∀ (n : nat), nat.le (nat.succ n) nat.zero ↔ false
 tactic.exfalso|tactic
 -- ENDFINDP
diff --git a/tests/lean/rw_set2.lean.expected.out b/tests/lean/rw_set2.lean.expected.out
index a11b1e10a..acf6d1958 100644
--- a/tests/lean/rw_set2.lean.expected.out
+++ b/tests/lean/rw_set2.lean.expected.out
@@ -1,4 +1,21 @@
+rewrite rules for iff
+#2, ?M_1 - ?M_2 < succ ?M_1 ↦ true
+#1, ?M_1 < 0 ↦ false
+#1, ?M_1 < succ ?M_1 ↦ true
+#1, ?M_1 < ?M_1 ↦ false
+#1, 0 < succ ?M_1 ↦ true
+#2, ?M_1 - ?M_2 ≤ ?M_1 ↦ true
+#2, ?M_2 ≤ max ?M_1 ?M_2 ↦ true
+#2, ?M_1 ≤ max ?M_1 ?M_2 ↦ true
+#1, 0 ≤ ?M_1 ↦ true
+#1, succ ?M_1 ≤ ?M_1 ↦ false
+#1, pred ?M_1 ≤ ?M_1 ↦ true
+#1, ?M_1 ≤ succ ?M_1 ↦ true
 rewrite rules for eq
 #1, g ?M_1 ↦ f ?M_1 + 1
 #2, g ?M_1 ↦ 1
 #2, f ?M_1 ↦ 0
+#1, max ?M_1 ?M_1 ↦ ?M_1
+#1, 0 - ?M_1 ↦ 0
+#2, succ ?M_1 - succ ?M_2 ↦ ?M_1 - ?M_2
+#4, ite ?M_1 ?M_4 ?M_4 ↦ ?M_4
diff --git a/tests/lean/rw_set3.lean.expected.out b/tests/lean/rw_set3.lean.expected.out
index a5353e9c2..2748bba11 100644
--- a/tests/lean/rw_set3.lean.expected.out
+++ b/tests/lean/rw_set3.lean.expected.out
@@ -1,2 +1,22 @@
+rewrite rules for iff
+#1, ?M_1 ↔ ?M_1 ↦ true
+#1, false ↔ ?M_1 ↦ ¬?M_1
+#1, ?M_1 ↔ false ↦ ¬?M_1
+#1, true ↔ ?M_1 ↦ ?M_1
+#1, ?M_1 ↔ true ↦ ?M_1
+#1, ?M_1 ∧ ?M_1 ↦ ?M_1
+#1, false ∧ ?M_1 ↦ false
+#1, ?M_1 ∧ false ↦ false
+#1, true ∧ ?M_1 ↦ ?M_1
+#1, ?M_1 ∧ true ↦ ?M_1
+#1, false ∨ ?M_1 ↦ ?M_1
+#1, ?M_1 ∨ false ↦ ?M_1
+#1, true ∨ ?M_1 ↦ true
+#1, ?M_1 ∨ true ↦ true
+#0, ¬false ↦ true
+#0, ¬true ↦ false
 rewrite rules for eq
 #2 perm, nat.add ?M_1 ?M_2 ↦ nat.add ?M_2 ?M_1
+#3, ite false ?M_2 ?M_3 ↦ ?M_3
+#3, ite true ?M_2 ?M_3 ↦ ?M_2
+#4, ite ?M_1 ?M_4 ?M_4 ↦ ?M_4