diff --git a/tests/lean/run/forest_height.lean b/tests/lean/run/forest_height.lean index aa9460f6a..574a55714 100644 --- a/tests/lean/run/forest_height.lean +++ b/tests/lean/run/forest_height.lean @@ -1,4 +1,4 @@ -import data.nat.basic data.sum data.sigma data.bool +import data.nat data.sum data.sigma data.bool open nat sigma inductive tree (A : Type) : Type := diff --git a/tests/lean/rw_set2.lean.expected.out b/tests/lean/rw_set2.lean.expected.out index acf6d1958..8844695bc 100644 --- a/tests/lean/rw_set2.lean.expected.out +++ b/tests/lean/rw_set2.lean.expected.out @@ -5,8 +5,6 @@ rewrite rules for iff #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 @@ -15,7 +13,6 @@ 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