From 29763190ad81409929b12628f85e6098e4626abd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Oct 2015 16:28:11 -0700 Subject: [PATCH] fix(tests/lean): adjust some tests to changes in the standard library --- tests/lean/630.lean.expected.out | 2 +- tests/lean/693.lean | 2 +- tests/lean/693.lean.expected.out | 4 ++-- tests/lean/793b.lean | 4 +++- tests/lean/793b.lean.expected.out | 2 +- tests/lean/K_bug.lean | 2 +- tests/lean/abbrev1.lean | 4 ++-- tests/lean/abbrev1.lean.expected.out | 4 ++-- tests/lean/coe.lean | 2 +- tests/lean/error_full_names.lean.expected.out | 11 +++-------- tests/lean/nat_pp.lean | 2 +- tests/lean/reserve_bugs.lean | 4 ++-- tests/lean/reserve_bugs.lean.expected.out | 8 ++++---- tests/lean/rw_set2.lean.expected.out | 12 ++++++------ tests/lean/uni_bug1.lean | 2 +- 15 files changed, 31 insertions(+), 34 deletions(-) diff --git a/tests/lean/630.lean.expected.out b/tests/lean/630.lean.expected.out index b2c738b68..39a1ffa02 100644 --- a/tests/lean/630.lean.expected.out +++ b/tests/lean/630.lean.expected.out @@ -1,5 +1,5 @@ definition pnat.pnat : Type₁ := -{n : ℕ | nat.gt n (nat.of_num 0)} +{n : ℕ | n > 0} inductive prod : Type → Type → Type constructors: prod.mk : Π {A : Type} {B : Type}, A → B → A × B diff --git a/tests/lean/693.lean b/tests/lean/693.lean index 34f9c9064..ef3008ecb 100644 --- a/tests/lean/693.lean +++ b/tests/lean/693.lean @@ -1,4 +1,4 @@ -open nat nat_esimp +open nat definition foo [unfold 1 3] (a : nat) (b : nat) (c :nat) : nat := (a + c) * b diff --git a/tests/lean/693.lean.expected.out b/tests/lean/693.lean.expected.out index b14394183..2e469dbec 100644 --- a/tests/lean/693.lean.expected.out +++ b/tests/lean/693.lean.expected.out @@ -1,7 +1,7 @@ 693.lean:10:2: proof state c : ℕ, h : c = 1 -⊢ 1 * c = 1 +⊢ foo 1 c 0 = foo 1 1 0 693.lean:18:2: proof state b c : ℕ, h : c = 1 @@ -13,4 +13,4 @@ h : c = 1 693.lean:34:2: proof state b c : ℕ, h : c = 1 -⊢ 2 * c = foo c 1 1 +⊢ foo 1 c 1 = foo c 1 1 diff --git a/tests/lean/793b.lean b/tests/lean/793b.lean index 55a15f50a..391c4504c 100644 --- a/tests/lean/793b.lean +++ b/tests/lean/793b.lean @@ -1 +1,3 @@ -check 1.2 +import data.rat +open rat +check (1.2:rat) diff --git a/tests/lean/793b.lean.expected.out b/tests/lean/793b.lean.expected.out index c4850ab8a..ad95b385e 100644 --- a/tests/lean/793b.lean.expected.out +++ b/tests/lean/793b.lean.expected.out @@ -1 +1 @@ -793b.lean:1:6: error: invalid decimal number, environment does not contain 'rat.of_num' (solution: use 'import data.rat') +6 / 5 : ℚ diff --git a/tests/lean/K_bug.lean b/tests/lean/K_bug.lean index b1299db12..6408d202a 100644 --- a/tests/lean/K_bug.lean +++ b/tests/lean/K_bug.lean @@ -11,7 +11,7 @@ theorem pred_succ (n : Nat) : pred (succ n) = n := rfl theorem succ.inj {n m : Nat} (H : succ n = succ m) : n = m := calc - n = pred (succ n) : pred_succ n⁻¹ + n = pred (succ n) : pred_succ n ... = pred (succ m) : {H} ... = m : pred_succ m diff --git a/tests/lean/abbrev1.lean b/tests/lean/abbrev1.lean index b2f739efe..a6e73b2e5 100644 --- a/tests/lean/abbrev1.lean +++ b/tests/lean/abbrev1.lean @@ -12,8 +12,8 @@ set_option pp.abbreviations true print definition tst -abbreviation id [parsing-only] {A : Type} (a : A) := a +abbreviation id [parsing_only] {A : Type} (a : A) := a -definition tst1 := id 10 +definition tst1 :nat := id 10 print definition tst1 diff --git a/tests/lean/abbrev1.lean.expected.out b/tests/lean/abbrev1.lean.expected.out index 0c3a8eb3d..984ab8f94 100644 --- a/tests/lean/abbrev1.lean.expected.out +++ b/tests/lean/abbrev1.lean.expected.out @@ -2,5 +2,5 @@ definition tst : ℕ (λ (a : Type₁), 2 + 3) ℕ definition tst : ℕ foo ℕ -definition tst1 : num -(λ (A : Type₁) (a : A), a) num 10 +definition tst1 : ℕ +(λ (A : Type₁) (a : A), a) ℕ 10 diff --git a/tests/lean/coe.lean b/tests/lean/coe.lean index 758f8b098..e530f6686 100644 --- a/tests/lean/coe.lean +++ b/tests/lean/coe.lean @@ -9,4 +9,4 @@ definition Functor.to_fun [coercion] (f : Functor) {A B : Type} : A → B := Functor.rec (λ f, f) f A B constant f : Functor -check f 0 = 0 +check f (0:num) = (0:num) diff --git a/tests/lean/error_full_names.lean.expected.out b/tests/lean/error_full_names.lean.expected.out index d1df57f0f..2f6e83394 100644 --- a/tests/lean/error_full_names.lean.expected.out +++ b/tests/lean/error_full_names.lean.expected.out @@ -1,11 +1,6 @@ -error_full_names.lean:4:8: error: type mismatch at application - 0 + nat.zero -term - nat.zero -has type - nat -but is expected to have type - ℕ +error_full_names.lean:4:8: error: failed to synthesize placeholder + +⊢ has_add nat error_full_names.lean:8:6: error: type mismatch at application nat.succ nat.zero term diff --git a/tests/lean/nat_pp.lean b/tests/lean/nat_pp.lean index 74968b0b1..1f2e4f91b 100644 --- a/tests/lean/nat_pp.lean +++ b/tests/lean/nat_pp.lean @@ -1,4 +1,4 @@ eval nat.add (nat.of_num 3) (nat.of_num 6) open nat eval nat.add (nat.of_num 3) (nat.of_num 6) -eval 3 + 6 +eval (3:nat) + 6 diff --git a/tests/lean/reserve_bugs.lean b/tests/lean/reserve_bugs.lean index 0bd501635..9f47b520c 100644 --- a/tests/lean/reserve_bugs.lean +++ b/tests/lean/reserve_bugs.lean @@ -17,9 +17,9 @@ infixr `&` := h set_option pp.notation false -check -1 + 2 +check -(1:num) + 2 check 1 & 2 & 3 & 4 -check 1 - 2 - 3 - 4 +check (1:num) - 2 - 3 - 4 infixr `~~`:60 := h infixl `!!`:60 := h diff --git a/tests/lean/reserve_bugs.lean.expected.out b/tests/lean/reserve_bugs.lean.expected.out index 107303f21..265bd32dc 100644 --- a/tests/lean/reserve_bugs.lean.expected.out +++ b/tests/lean/reserve_bugs.lean.expected.out @@ -1,6 +1,6 @@ -g (f 1) 2 : num +add (f 1) 2 : num +h 1 (h 2 (h 3 4)) : num +sub (sub (sub 1 2) 3) 4 : num h 1 (h 2 (h 3 4)) : num h (h (h 1 2) 3) 4 : num -h 1 (h 2 (h 3 4)) : num -h (h (h 1 2) 3) 4 : num -h 1 (h (g 2 3) 4) : num +h 1 (h (add 2 3) 4) : num diff --git a/tests/lean/rw_set2.lean.expected.out b/tests/lean/rw_set2.lean.expected.out index c06137f93..288702e14 100644 --- a/tests/lean/rw_set2.lean.expected.out +++ b/tests/lean/rw_set2.lean.expected.out @@ -1,18 +1,18 @@ simplification 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 #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 +#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 simplification rules for eq #1, g ?M_1 ↦ f ?M_1 + 1 #2, g ?M_1 ↦ 1 #2, f ?M_1 ↦ 0 +#4, ite ?M_1 ?M_4 ?M_4 ↦ ?M_4 #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/uni_bug1.lean b/tests/lean/uni_bug1.lean index e54fc08c1..4d839b544 100644 --- a/tests/lean/uni_bug1.lean +++ b/tests/lean/uni_bug1.lean @@ -6,4 +6,4 @@ constant f (a b : nat) (H : R a b) : nat axiom Rtrue (a b : nat) : R a b -check f 1 0 (Rtrue (pr1 (pair 1 0)) 0) +check f 1 0 (Rtrue (pr1 (pair 1 (0:nat))) 0)