fix(tests/lean): adjust some tests to changes in the standard library

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

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

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

tests/lean/793b.lean

@@ -1 +1,3 @@
-check 1.2
+import data.rat
+open rat
+check (1.2:rat)

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 : ℚ

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
 

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

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

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)

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

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

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

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

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

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)