From 989a2e077bf0e94b00bd267c19f76ac23284057d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 22 Nov 2015 17:15:28 -0800
Subject: [PATCH] fix(tests/lean): adjust tests

---
 tests/lean/interactive/findp.input.expected.out | 2 +-
 tests/lean/rw_set2.lean.expected.out            | 4 ++++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/tests/lean/interactive/findp.input.expected.out b/tests/lean/interactive/findp.input.expected.out
index d0adf68a4..feda13f33 100644
--- a/tests/lean/interactive/findp.input.expected.out
+++ b/tests/lean/interactive/findp.input.expected.out
@@ -17,7 +17,7 @@ true_ne_false|¬true = false
 nat.lt_self_iff_false|∀ (n : ℕ), n < n ↔ false
 iff_false|∀ (a : Prop), a ↔ false ↔ ¬a
 true_iff_false|true ↔ false ↔ false
-ne_self_iff_false|∀ (a : ?A), a ≠ a ↔ false
+ne_self_iff_false|∀ (a : ?A), ¬a = a ↔ false
 not_of_is_false|is_false ?c → ¬?c
 or_false|∀ (a : Prop), a ∨ false ↔ a
 not_of_iff_false|(?a ↔ false) → ¬?a
diff --git a/tests/lean/rw_set2.lean.expected.out b/tests/lean/rw_set2.lean.expected.out
index 7c347aef4..afeeec5c8 100644
--- a/tests/lean/rw_set2.lean.expected.out
+++ b/tests/lean/rw_set2.lean.expected.out
@@ -6,6 +6,7 @@ simplification rules for iff
 #1, ?M_1 ↔ true ↦ ?M_1
 #0, false ↔ true ↦ false
 #0, true ↔ false ↦ false
+#1, ¬?M_1 ↔ ?M_1 ↦ false
 #1, ?M_1 ↔ ¬?M_1 ↦ false
 #2, ?M_1 - ?M_2 ≤ ?M_1 ↦ true
 #1, 0 ≤ ?M_1 ↦ true
@@ -13,6 +14,8 @@ simplification rules for iff
 #1, pred ?M_1 ≤ ?M_1 ↦ true
 #1, ?M_1 ≤ succ ?M_1 ↦ true
 #1, ?M_1 ∧ ?M_1 ↦ ?M_1
+#1, ?M_1 ∧ ¬?M_1 ↦ false
+#1, ¬?M_1 ∧ ?M_1 ↦ false
 #1, false ∧ ?M_1 ↦ false
 #1, ?M_1 ∧ false ↦ false
 #1, true ∧ ?M_1 ↦ ?M_1
@@ -34,6 +37,7 @@ simplification rules for iff
 #3, (?M_1 ∨ ?M_2) ∨ ?M_3 ↦ ?M_1 ∨ ?M_2 ∨ ?M_3
 #2 perm, ?M_1 ∨ ?M_2 ↦ ?M_2 ∨ ?M_1
 #2, ?M_2 = ?M_2 ↦ true
+#2, ¬?M_2 = ?M_2 ↦ false
 #0, ¬false ↦ true
 #0, ¬true ↦ false
 simplification rules for eq