From 23dd47d27fbe411a1b2c68e19175ec9fc06a4dd8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 19 Jul 2015 21:32:42 -0700 Subject: [PATCH] fix(tests/lean): adjust tests to recent changes to the standard library --- tests/lean/run/forest_height.lean | 2 +- tests/lean/rw_set2.lean.expected.out | 3 --- 2 files changed, 1 insertion(+), 4 deletions(-) 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