diff --git a/tests/lean/671.lean.expected.out b/tests/lean/671.lean.expected.out
index 869b128ec..d1e192519 100644
--- a/tests/lean/671.lean.expected.out
+++ b/tests/lean/671.lean.expected.out
@@ -1,2 +1,2 @@
-definition nat.add : nat → nat → nat :=
-λ (a b : nat), nat.rec_on b a (λ (b₁ : nat), nat.succ)
+definition nat.add : ℕ → ℕ → ℕ :=
+λ (a b : ℕ), nat.rec_on b a (λ (b₁ : ℕ), nat.succ)
diff --git a/tests/lean/bad_structures2.lean.expected.out b/tests/lean/bad_structures2.lean.expected.out
index 653deefb3..714cda658 100644
--- a/tests/lean/bad_structures2.lean.expected.out
+++ b/tests/lean/bad_structures2.lean.expected.out
@@ -1,7 +1,7 @@
 bad_structures2.lean:7:27: error: invalid 'structure' header, field 'x' from 'boo' has already been declared with a different type
   bool
 and
-  nat
+  ℕ
 bad_structures2.lean:12:27: error: invalid 'structure' header, field 'x' has already been declared with a different binder annotation
 bad_structures2.lean:15:1: error: field 'x' has been declared in parent structure
 bad_structures2.lean:18:2: error: invalid field, identifier expected
diff --git a/tests/lean/constr_tac_errors.lean.expected.out b/tests/lean/constr_tac_errors.lean.expected.out
index 596992e29..4e5910cef 100644
--- a/tests/lean/constr_tac_errors.lean.expected.out
+++ b/tests/lean/constr_tac_errors.lean.expected.out
@@ -1,10 +1,10 @@
 constr_tac_errors.lean:3:2: error:invalid 'constructor' tactic, goal is an inductive datatype, but it does not have 1 constructor(s)
 proof state:
 
-⊢ nat
+⊢ ℕ
 constr_tac_errors.lean:4:0: error: don't know how to synthesize placeholder
 
-⊢ nat
+⊢ ℕ
 constr_tac_errors.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   ?M_1
@@ -47,10 +47,10 @@ remark: set 'formatter.hide_full_terms' to false to see the complete term
 constr_tac_errors.lean:39:2: error:invalid 'constructor' tactic, goal is not an inductive datatype
 proof state:
 
-⊢ nat → nat
+⊢ ℕ → ℕ
 constr_tac_errors.lean:40:0: error: don't know how to synthesize placeholder
 
-⊢ nat → nat
+⊢ ℕ → ℕ
 constr_tac_errors.lean:40:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   ?M_1
diff --git a/tests/lean/ctx.lean.expected.out b/tests/lean/ctx.lean.expected.out
index 37fd96775..05a7d792a 100644
--- a/tests/lean/ctx.lean.expected.out
+++ b/tests/lean/ctx.lean.expected.out
@@ -1,10 +1,10 @@
 ctx.lean:3:0: error: don't know how to synthesize placeholder
 A B : Type,
-a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 : nat,
+a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 : ℕ,
 b1 b2 b3 : bool,
 h : A = B,
 p1 p2 : A × B
-⊢ nat
+⊢ ℕ
 ctx.lean:3:0: error: failed to add declaration 'foo' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   ?M_1
diff --git a/tests/lean/error_full_names.lean.expected.out b/tests/lean/error_full_names.lean.expected.out
index 81bb5d2d1..d1df57f0f 100644
--- a/tests/lean/error_full_names.lean.expected.out
+++ b/tests/lean/error_full_names.lean.expected.out
@@ -11,6 +11,6 @@ error_full_names.lean:8:6: error: type mismatch at application
 term
   nat.zero
 has type
-  foo.nat
-but is expected to have type
   nat
+but is expected to have type
+  ℕ
diff --git a/tests/lean/errors.lean.expected.out b/tests/lean/errors.lean.expected.out
index 9703f2727..4d018e263 100644
--- a/tests/lean/errors.lean.expected.out
+++ b/tests/lean/errors.lean.expected.out
@@ -1,5 +1,5 @@
 errors.lean:4:0: error: unknown identifier 'a'
-tst1 : nat → nat → nat
+tst1 : ℕ → ℕ → ℕ
 errors.lean:12:8: error: unknown identifier 'add'
 errors.lean:22:12: error: unknown identifier 'b'
 tst3 : A → A → A
diff --git a/tests/lean/exact_partial2.lean.expected.out b/tests/lean/exact_partial2.lean.expected.out
index 9e9bb0e70..88108c524 100644
--- a/tests/lean/exact_partial2.lean.expected.out
+++ b/tests/lean/exact_partial2.lean.expected.out
@@ -1,17 +1,17 @@
 exact_partial2.lean:3:21: error: don't know how to synthesize placeholder
-a b c : nat,
+a b c : ℕ,
 h₁ : a = b,
 h₂ : b = c
 ⊢ b = c
 exact_partial2.lean:3:2: error:invalid 'exact' tactic, term still contains metavariables after elaboration
   eq.trans h₁ ?M_1
 proof state:
-a b c : nat,
+a b c : ℕ,
 h₁ : a = b,
 h₂ : b = c
 ⊢ a = c
 exact_partial2.lean:4:0: error: don't know how to synthesize placeholder
-a b c : nat,
+a b c : ℕ,
 h₁ : a = b,
 h₂ : b = c
 ⊢ a = c
diff --git a/tests/lean/have_tactic.lean.expected.out b/tests/lean/have_tactic.lean.expected.out
index d152d5ac2..08ac2a380 100644
--- a/tests/lean/have_tactic.lean.expected.out
+++ b/tests/lean/have_tactic.lean.expected.out
@@ -1,17 +1,17 @@
 have_tactic.lean:4:31: error: don't know how to synthesize placeholder
-a b c : nat,
+a b c : ℕ,
 h₁ : a = b,
 h₂ : b = c
 ⊢ b = c
 have_tactic.lean:4:19: error:invalid 'exact' tactic, term still contains metavariables after elaboration
   eq.trans h₁ ?M_1
 proof state:
-a b c : nat,
+a b c : ℕ,
 h₁ : a = b,
 h₂ : b = c
 ⊢ a = c
 have_tactic.lean:5:0: error: don't know how to synthesize placeholder
-a b c : nat
+a b c : ℕ
 ⊢ a = b → b = c → a = c
 have_tactic.lean:5:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
diff --git a/tests/lean/interactive/findp.input.expected.out b/tests/lean/interactive/findp.input.expected.out
index c586e7f5c..25e5ce314 100644
--- a/tests/lean/interactive/findp.input.expected.out
+++ b/tests/lean/interactive/findp.input.expected.out
@@ -9,15 +9,15 @@ false.rec_on|Π (C : Type), false → C
 false.cases_on|Π (C : Type), false → C
 false.induction_on|∀ (C : Prop), false → C
 true_ne_false|¬true = false
-nat.lt_self_iff_false|∀ (n : nat), nat.lt n n ↔ false
+nat.lt_self_iff_false|∀ (n : ℕ), nat.lt n n ↔ false
 not_of_is_false|is_false ?c → ¬?c
 not_of_iff_false|(?a ↔ false) → ¬?a
 is_false|Π (c : Prop) [H : decidable c], Prop
 classical.eq_true_or_eq_false|∀ (a : Prop), a = true ∨ a = false
 classical.eq_false_or_eq_true|∀ (a : Prop), a = false ∨ a = true
-nat.lt_zero_iff_false|∀ (a : nat), nat.lt a nat.zero ↔ false
+nat.lt_zero_iff_false|∀ (a : ℕ), nat.lt a nat.zero ↔ false
 not_of_eq_false|?p = false → ¬?p
-nat.succ_le_self_iff_false|∀ (n : nat), nat.le (nat.succ n) n ↔ false
+nat.succ_le_self_iff_false|∀ (n : ℕ), nat.le (nat.succ n) n ↔ false
 decidable.rec_on_false|Π (H3 : ¬?p), ?H2 H3 → decidable.rec_on ?H ?H1 ?H2
 not_false|¬false
 decidable_false|decidable false
@@ -25,6 +25,6 @@ of_not_is_false|¬is_false ?c → ?c
 classical.cases_true_false|∀ (P : Prop → Prop), P true → P false → (∀ (a : Prop), P a)
 iff_false_intro|¬?a → (?a ↔ false)
 ne_false_of_self|?p → ?p ≠ false
-nat.succ_le_zero_iff_false|∀ (n : nat), nat.le (nat.succ n) nat.zero ↔ false
+nat.succ_le_zero_iff_false|∀ (n : ℕ), nat.le (nat.succ n) nat.zero ↔ false
 tactic.exfalso|tactic
 -- ENDFINDP
diff --git a/tests/lean/mismatch.lean.expected.out b/tests/lean/mismatch.lean.expected.out
index c26c9c85c..a8ea208ea 100644
--- a/tests/lean/mismatch.lean.expected.out
+++ b/tests/lean/mismatch.lean.expected.out
@@ -1,8 +1,8 @@
 mismatch.lean:3:7: error: type mismatch at application
-  @id nat 1
+  @id ℕ 1
 term
   1
 has type
   num
 but is expected to have type
-  nat
+  ℕ
diff --git a/tests/lean/quasireducible.lean.expected.out b/tests/lean/quasireducible.lean.expected.out
index 575306a90..64f286a05 100644
--- a/tests/lean/quasireducible.lean.expected.out
+++ b/tests/lean/quasireducible.lean.expected.out
@@ -2,11 +2,11 @@ quasireducible.lean:11:11: error:invalid 'rewrite' tactic, rewrite step failed u
   f a
 no subterm in the goal matched the pattern
 proof state:
-a : nat,
+a : ℕ,
 H : f a = a
 ⊢ g a = a
 quasireducible.lean:11:0: error: don't know how to synthesize placeholder
-a : nat,
+a : ℕ,
 H : f a = a
 ⊢ g a = a
 quasireducible.lean:11:0: error: failed to add declaration 'example' to environment, value has metavariables
@@ -16,11 +16,11 @@ quasireducible.lean:16:11: error:invalid 'rewrite' tactic, rewrite step failed u
   f a
 no subterm in the goal matched the pattern
 proof state:
-a : nat,
+a : ℕ,
 H : f a = a
 ⊢ g a = a
 quasireducible.lean:16:0: error: don't know how to synthesize placeholder
-a : nat,
+a : ℕ,
 H : f a = a
 ⊢ g a = a
 quasireducible.lean:16:0: error: failed to add declaration 'example' to environment, value has metavariables
diff --git a/tests/lean/revert_fail.lean.expected.out b/tests/lean/revert_fail.lean.expected.out
index 38cb41329..759ccec9a 100644
--- a/tests/lean/revert_fail.lean.expected.out
+++ b/tests/lean/revert_fail.lean.expected.out
@@ -1,12 +1,12 @@
 revert_fail.lean:5:2: error:invalid 'revert' tactic, hypothesis 'v' depends on 'n'
 proof state:
 A : Type,
-n : nat,
+n : ℕ,
 v : vector A n
 ⊢ v = v
 revert_fail.lean:6:0: error: don't know how to synthesize placeholder
 A : Type,
-n : nat,
+n : ℕ,
 v : vector A n
 ⊢ v = v
 revert_fail.lean:6:0: error: failed to add declaration 'example' to environment, value has metavariables
@@ -16,17 +16,17 @@ revert_fail.lean:11:2: error:invalid tactic, there are no goals to be solved
 proof state:
 no goals
 revert_fail.lean:12:0: error: don't know how to synthesize placeholder
-n : nat
+n : ℕ
 ⊢ n = n
 revert_fail.lean:12:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   ?M_1
 revert_fail.lean:16:2: error:invalid 'revert' tactic, unknown hypothesis 'm'
 proof state:
-n : nat
+n : ℕ
 ⊢ n = n
 revert_fail.lean:17:0: error: don't know how to synthesize placeholder
-n : nat
+n : ℕ
 ⊢ n = n
 revert_fail.lean:17:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
diff --git a/tests/lean/slow/nat_bug2.lean b/tests/lean/slow/nat_bug2.lean
index 9eaf20e44..70b70eabe 100644
--- a/tests/lean/slow/nat_bug2.lean
+++ b/tests/lean/slow/nat_bug2.lean
@@ -83,7 +83,7 @@ theorem succ_ne_self (n : ℕ) : succ n ≠ n
       absurd H ne)
     (take k IH H, IH (succ.inj H))
 
-theorem decidable_eq [instance] (n m : ℕ) : decidable (n = m)
+theorem decidable_eq [instance] (n m : nat) : decidable (n = m)
 := have general : ∀n, decidable (n = m), from
      nat.rec_on m
        (take n,
diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean
index 801ac3fec..9f21880d7 100644
--- a/tests/lean/slow/nat_wo_hints.lean
+++ b/tests/lean/slow/nat_wo_hints.lean
@@ -77,7 +77,7 @@ theorem succ_ne_self (n : ℕ) : succ n ≠ n
       absurd H ne)
     (take k IH H, IH (succ.inj H))
 
-theorem decidable_eq [instance] (n m : ℕ) : decidable (n = m)
+theorem decidable_eq [instance] (n m : nat) : decidable (n = m)
 := have general : ∀n, decidable (n = m), from
      nat.rec_on m
        (take n,
diff --git a/tests/lean/subst_bug.lean.expected.out b/tests/lean/subst_bug.lean.expected.out
index 8b01280ca..f277f7730 100644
--- a/tests/lean/subst_bug.lean.expected.out
+++ b/tests/lean/subst_bug.lean.expected.out
@@ -1,12 +1,12 @@
 subst_bug.lean:4:2: error:invalid 'subst' tactic, 'a' occurs in the other side of the equation
 proof state:
-f : nat → nat,
-a b : nat,
+f : ℕ → ℕ,
+a b : ℕ,
 h₁ : f a = a
 ⊢ f (f a) = a
 subst_bug.lean:5:0: error: don't know how to synthesize placeholder
-f : nat → nat,
-a b : nat
+f : ℕ → ℕ,
+a b : ℕ
 ⊢ f a = a → f (f a) = a
 subst_bug.lean:5:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
diff --git a/tests/lean/unsolved_proof_qed.lean.expected.out b/tests/lean/unsolved_proof_qed.lean.expected.out
index cfa473b58..481cc36c8 100644
--- a/tests/lean/unsolved_proof_qed.lean.expected.out
+++ b/tests/lean/unsolved_proof_qed.lean.expected.out
@@ -1,17 +1,17 @@
 unsolved_proof_qed.lean:2:18: error: don't know how to synthesize placeholder
-a b c : nat,
+a b c : ℕ,
 H₁ : a = b,
 H₂ : b = c
 ⊢ b = c
 unsolved_proof_qed.lean:2:0: error:invalid 'exact' tactic, term still contains metavariables after elaboration
   eq.trans H₁ ?M_1
 proof state:
-a b c : nat,
+a b c : ℕ,
 H₁ : a = b,
 H₂ : b = c
 ⊢ a = c
 unsolved_proof_qed.lean:2:0: error: don't know how to synthesize placeholder
-a b c : nat,
+a b c : ℕ,
 H₁ : a = b,
 H₂ : b = c
 ⊢ a = c
@@ -19,23 +19,23 @@ unsolved_proof_qed.lean:2:0: error: failed to add declaration 'example' to envir
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   ?M_1
 unsolved_proof_qed.lean:5:33: error: don't know how to synthesize placeholder
-a b c : nat,
+a b c : ℕ,
 H₁ : a = b,
 H₂ : b = c
 ⊢ c = b
 unsolved_proof_qed.lean:5:18: error:invalid 'exact' tactic, term still contains metavariables after elaboration
   eq.trans ?M_1 (eq.symm H₁)
 proof state:
-a b c : nat,
+a b c : ℕ,
 H₁ : a = b,
 H₂ : b = c
 ⊢ c = a
 unsolved_proof_qed.lean:5:18: error: don't know how to synthesize placeholder
-a b c : nat,
+a b c : ℕ,
 H₁ : a = b,
 H₂ : b = c
 ⊢ c = a
 unsolved_proof_qed.lean:5:0: error: failed to add declaration 'example' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
-  λ (a b c : nat) (H₁ : …) (H₂ : …),
+  λ (a b c : ℕ) (H₁ : …) (H₂ : …),
     … ?M_1
diff --git a/tests/lean/urec.lean.expected.out b/tests/lean/urec.lean.expected.out
index 2534a43fc..357e76c28 100644
--- a/tests/lean/urec.lean.expected.out
+++ b/tests/lean/urec.lean.expected.out
@@ -20,9 +20,9 @@ recursor information
   major premise pos.:       2
   dep. elimination:         1
 vector.induction_on.{l_1} :
-  ∀ {A : Type.{l_1}} {C : Π (a : nat), vector.{l_1} A a → Prop} {a : nat} (n : vector.{l_1} A a),
+  ∀ {A : Type.{l_1}} {C : Π (a : ℕ), vector.{l_1} A a → Prop} {a : ℕ} (n : vector.{l_1} A a),
     C nat.zero (@vector.nil.{l_1} A) →
-    (∀ {n : nat} (a : A) (a_1 : vector.{l_1} A n), C n a_1 → C (nat.succ n) (@vector.cons.{l_1} A n a a_1)) →
+    (∀ {n : ℕ} (a : A) (a_1 : vector.{l_1} A n), C n a_1 → C (nat.succ n) (@vector.cons.{l_1} A n a a_1)) →
     C a n
 recursor information
   num. parameters:          1