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)