diff --git a/src/Init/Data/Array.lean b/src/Init/Data/Array.lean
index df9ed67253..dbeeda4f07 100644
--- a/src/Init/Data/Array.lean
+++ b/src/Init/Data/Array.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
diff --git a/src/Init/Data/Basic.lean b/src/Init/Data/Basic.lean
index ea963f66b3..e7d7f7ae91 100644
--- a/src/Init/Data/Basic.lean
+++ b/src/Init/Data/Basic.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
diff --git a/src/Init/Data/ByteArray.lean b/src/Init/Data/ByteArray.lean
index b6ee6ccf4b..80c62ed57e 100644
--- a/src/Init/Data/ByteArray.lean
+++ b/src/Init/Data/ByteArray.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
diff --git a/src/Init/Data/Char.lean b/src/Init/Data/Char.lean
index dc2257bbfe..c0c124acfc 100644
--- a/src/Init/Data/Char.lean
+++ b/src/Init/Data/Char.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
diff --git a/src/Init/Data/Fin.lean b/src/Init/Data/Fin.lean
index 4e571c0f4b..6e2c8a6fba 100644
--- a/src/Init/Data/Fin.lean
+++ b/src/Init/Data/Fin.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean
index 6ed526daab..9c3f611a9c 100644
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -8,12 +9,12 @@ import Init.Core
 import Init.Data.ToString.Basic
 
 structure FloatSpec :=
-(float : Type)
-(val   : float)
-(lt    : float → float → Prop)
-(le    : float → float → Prop)
-(decLt : DecidableRel lt)
-(decLe : DecidableRel le)
+  (float : Type)
+  (val   : float)
+  (lt    : float → float → Prop)
+  (le    : float → float → Prop)
+  (decLt : DecidableRel lt)
+  (decLe : DecidableRel le)
 
 -- Just show FloatSpec is inhabited.
 constant floatSpec : FloatSpec := {
@@ -26,21 +27,23 @@ constant floatSpec : FloatSpec := {
 }
 
 structure Float :=
-(val : floatSpec.float)
+  (val : floatSpec.float)
 
 instance : Inhabited Float := ⟨{ val := floatSpec.val }⟩
 
-@[extern "lean_float_of_nat"] constant Float.ofNat : (@& Nat) → Float := arbitrary _
-@[extern c inline "#1 + #2"]  constant Float.add : Float → Float → Float := arbitrary _
-@[extern c inline "#1 - #2"]  constant Float.sub : Float → Float → Float := arbitrary _
-@[extern c inline "#1 * #2"]  constant Float.mul : Float → Float → Float := arbitrary _
-@[extern c inline "#1 / #2"]  constant Float.div : Float → Float → Float := arbitrary _
+@[extern "lean_float_of_nat"] constant Float.ofNat : (@& Nat) → Float
+@[extern c inline "#1 + #2"]  constant Float.add : Float → Float → Float
+@[extern c inline "#1 - #2"]  constant Float.sub : Float → Float → Float
+@[extern c inline "#1 * #2"]  constant Float.mul : Float → Float → Float
+@[extern c inline "#1 / #2"]  constant Float.div : Float → Float → Float
 
-def Float.lt  : Float → Float → Prop :=
-fun a b => match a, b with
-| ⟨a⟩, ⟨b⟩ => floatSpec.lt a b
+set_option bootstrap.gen_matcher_code false
+def Float.lt  : Float → Float → Prop := fun a b =>
+  match a, b with
+  | ⟨a⟩, ⟨b⟩ => floatSpec.lt a b
 
-def Float.le  : Float → Float → Prop := fun a b => floatSpec.le a.val b.val
+def Float.le  : Float → Float → Prop := fun a b =>
+  floatSpec.le a.val b.val
 
 instance : HasZero Float   := ⟨Float.ofNat 0⟩
 instance : HasOne Float    := ⟨Float.ofNat 1⟩
@@ -52,48 +55,48 @@ instance : HasDiv Float    := ⟨Float.div⟩
 instance : HasLess Float   := ⟨Float.lt⟩
 instance : HasLessEq Float := ⟨Float.le⟩
 
-@[extern c inline "#1 == #2"] constant Float.beq (a b : Float) : Bool := arbitrary _
+@[extern c inline "#1 == #2"] constant Float.beq (a b : Float) : Bool
 
 instance : HasBeq Float := ⟨Float.beq⟩
 
 @[extern c inline "#1 < #2"]   constant Float.decLt (a b : Float) : Decidable (a < b) :=
-match a, b with
-| ⟨a⟩, ⟨b⟩ => floatSpec.decLt a b
+  match a, b with
+  | ⟨a⟩, ⟨b⟩ => floatSpec.decLt a b
 
 @[extern c inline "#1 <= #2"] constant Float.decLe (a b : Float) : Decidable (a ≤ b) :=
-match a, b with
-| ⟨a⟩, ⟨b⟩ => floatSpec.decLe a b
+  match a, b with
+  | ⟨a⟩, ⟨b⟩ => floatSpec.decLe a b
 
 instance floatDecLt (a b : Float) : Decidable (a < b) := Float.decLt a b
 instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b
 
-@[extern "lean_float_to_string"] constant Float.toString : Float → String := arbitrary _
+@[extern "lean_float_to_string"] constant Float.toString : Float → String
 
 instance : HasToString Float := ⟨Float.toString⟩
 
 abbrev Nat.toFloat (n : Nat) : Float :=
-Float.ofNat n
+  Float.ofNat n
 
-@[extern "sin"] constant Float.sin : Float → Float := arbitrary _
-@[extern "cos"] constant Float.cos : Float → Float := arbitrary _
-@[extern "tan"] constant Float.tan : Float → Float := arbitrary _
-@[extern "asin"] constant Float.asin : Float → Float := arbitrary _
-@[extern "acos"] constant Float.acos : Float → Float := arbitrary _
-@[extern "atan"] constant Float.atan : Float → Float := arbitrary _
-@[extern "atan2"] constant Float.atan2 : Float → Float → Float := arbitrary _
-@[extern "sinh"] constant Float.sinh : Float → Float := arbitrary _
-@[extern "cosh"] constant Float.cosh : Float → Float := arbitrary _
-@[extern "tanh"] constant Float.tanh : Float → Float := arbitrary _
-@[extern "asinh"] constant Float.asinh : Float → Float := arbitrary _
-@[extern "acosh"] constant Float.acosh : Float → Float := arbitrary _
-@[extern "atanh"] constant Float.atanh : Float → Float := arbitrary _
-@[extern "exp"] constant Float.exp : Float → Float := arbitrary _
-@[extern "exp2"] constant Float.exp2 : Float → Float := arbitrary _
-@[extern "log"] constant Float.log : Float → Float := arbitrary _
-@[extern "log2"] constant Float.log2 : Float → Float := arbitrary _
-@[extern "log10"] constant Float.log10 : Float → Float := arbitrary _
-@[extern "pow"] constant Float.pow : Float → Float → Float := arbitrary _
-@[extern "sqrt"] constant Float.sqrt : Float → Float := arbitrary _
-@[extern "cbrt"] constant Float.cbrt : Float → Float := arbitrary _
+@[extern "sin"] constant Float.sin : Float → Float
+@[extern "cos"] constant Float.cos : Float → Float
+@[extern "tan"] constant Float.tan : Float → Float
+@[extern "asin"] constant Float.asin : Float → Float
+@[extern "acos"] constant Float.acos : Float → Float
+@[extern "atan"] constant Float.atan : Float → Float
+@[extern "atan2"] constant Float.atan2 : Float → Float → Float
+@[extern "sinh"] constant Float.sinh : Float → Float
+@[extern "cosh"] constant Float.cosh : Float → Float
+@[extern "tanh"] constant Float.tanh : Float → Float
+@[extern "asinh"] constant Float.asinh : Float → Float
+@[extern "acosh"] constant Float.acosh : Float → Float
+@[extern "atanh"] constant Float.atanh : Float → Float
+@[extern "exp"] constant Float.exp : Float → Float
+@[extern "exp2"] constant Float.exp2 : Float → Float
+@[extern "log"] constant Float.log : Float → Float
+@[extern "log2"] constant Float.log2 : Float → Float
+@[extern "log10"] constant Float.log10 : Float → Float
+@[extern "pow"] constant Float.pow : Float → Float → Float
+@[extern "sqrt"] constant Float.sqrt : Float → Float
+@[extern "cbrt"] constant Float.cbrt : Float → Float
 
 instance : HasPow Float Float := ⟨Float.pow⟩
diff --git a/src/Init/Data/FloatArray.lean b/src/Init/Data/FloatArray.lean
index 7c798deaa3..50f84cee3e 100644
--- a/src/Init/Data/FloatArray.lean
+++ b/src/Init/Data/FloatArray.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
diff --git a/src/Init/Data/Hashable.lean b/src/Init/Data/Hashable.lean
index b9c851d3ae..cb0964628b 100644
--- a/src/Init/Data/Hashable.lean
+++ b/src/Init/Data/Hashable.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -9,32 +10,36 @@ import Init.Data.String
 universes u
 
 class Hashable (α : Type u) :=
-(hash : α → USize)
+  (hash : α → USize)
 
 export Hashable (hash)
 
 @[extern "lean_usize_mix_hash"]
-constant mixHash (u₁ u₂ : USize) : USize := arbitrary _
+constant mixHash (u₁ u₂ : USize) : USize
 
 @[extern "lean_string_hash"]
-protected constant String.hash (s : @& String) : USize := arbitrary _
+protected constant String.hash (s : @& String) : USize
+
 instance : Hashable String := ⟨String.hash⟩
 
-protected def Nat.hash (n : Nat) : USize :=
-USize.ofNat n
+instance : Hashable Nat := {
+  hash := fun n => USize.ofNat n
+}
 
-instance : Hashable Nat := ⟨Nat.hash⟩
+instance {α β} [Hashable α] [Hashable β] : Hashable (α × β) := {
+  hash := fun (a, b) => mixHash (hash a) (hash b)
+}
 
-instance {α β} [Hashable α] [Hashable β] : Hashable (α × β) :=
-⟨fun ⟨a, b⟩ => mixHash (hash a) (hash b)⟩
+protected def Option.hash {α} [Hashable α] : Option α → USize
+  | none   => 11
+  | some a => mixHash (hash a) 13
 
-def Option.hash {α} [Hashable α] : Option α → USize
-| none   => 11
-| some a => mixHash (hash a) 13
+instance {α} [Hashable α] : Hashable (Option α) := {
+  hash := fun
+    | none   => 11
+    | some a => mixHash (hash a) 13
+}
 
-instance {α} [Hashable α] : Hashable (Option α) := ⟨Option.hash⟩
-
-def List.hash {α} [Hashable α] (as : List α) : USize :=
-as.foldl (fun r a => mixHash r (hash a)) 7
-
-instance {α} [Hashable α] : Hashable (List α) := ⟨List.hash⟩
+instance {α} [Hashable α] : Hashable (List α) := {
+  hash := fun as => as.foldl (fun r a => mixHash r (hash a)) 7
+}
diff --git a/src/Init/Data/Int.lean b/src/Init/Data/Int.lean
index 55959e95bd..92aacbb503 100644
--- a/src/Init/Data/Int.lean
+++ b/src/Init/Data/Int.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
diff --git a/src/Init/Data/List.lean b/src/Init/Data/List.lean
index 6bb2c73169..e95fbb5e58 100644
--- a/src/Init/Data/List.lean
+++ b/src/Init/Data/List.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
diff --git a/src/Init/Data/Nat.lean b/src/Init/Data/Nat.lean
index cf7be93c6e..955ecfb743 100644
--- a/src/Init/Data/Nat.lean
+++ b/src/Init/Data/Nat.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
diff --git a/src/Init/Data/Option.lean b/src/Init/Data/Option.lean
index 0a35feacc2..1df3f90d6c 100644
--- a/src/Init/Data/Option.lean
+++ b/src/Init/Data/Option.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
diff --git a/src/Init/Data/Range.lean b/src/Init/Data/Range.lean
index eababa8ce9..58f362b734 100644
--- a/src/Init/Data/Range.lean
+++ b/src/Init/Data/Range.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -5,29 +6,28 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.LeanInit
-new_frontend
 
 namespace Std
 -- We put `Range` in `Init` because we want the notation `[i:j]`  without importing `Std`
 -- We don't put `Range` in the top-level namespace to avoid collisions with user defined types
 structure Range :=
-(start : Nat := 0)
-(stop  : Nat)
-(step  : Nat := 1)
+  (start : Nat := 0)
+  (stop  : Nat)
+  (step  : Nat := 1)
 
 namespace Range
 universes u v
 
 @[inline] def forIn {β : Type u} {m : Type u → Type v} [Monad m] (range : Range) (init : β) (f : Nat → β → m (ForInStep β)) : m β :=
-let rec @[specialize] loop (i : Nat) (j : Nat) (b : β) : m β := do
-  if j ≥ range.stop then
-    pure b
-  else match i with
-   | 0   => pure b
-   | i+1 => match ← f j b with
-      | ForInStep.done b  => pure b
-      | ForInStep.yield b => loop i (j + range.step) b
-loop range.stop range.start init
+  let rec @[specialize] loop (i : Nat) (j : Nat) (b : β) : m β := do
+    if j ≥ range.stop then
+      pure b
+    else match i with
+     | 0   => pure b
+     | i+1 => match ← f j b with
+        | ForInStep.done b  => pure b
+        | ForInStep.yield b => loop i (j + range.step) b
+  loop range.stop range.start init
 
 syntax:max "[" ":" term "]" : term
 syntax:max "[" term ":" term "]" : term
@@ -35,10 +35,10 @@ syntax:max "[" ":" term ":" term "]" : term
 syntax:max "[" term ":" term ":" term "]" : term
 
 macro_rules
-| `([ : $stop]) => `({ stop := $stop : Range })
-| `([ $start : $stop ]) => `({ start := $start, stop := $stop : Range })
-| `([ $start : $stop : $step ]) => `({ start := $start, stop := $stop, step := $step : Range })
-| `([ : $stop : $step ]) => `({ stop := $stop, step := $step : Range })
+  | `([ : $stop]) => `({ stop := $stop : Range })
+  | `([ $start : $stop ]) => `({ start := $start, stop := $stop : Range })
+  | `([ $start : $stop : $step ]) => `({ start := $start, stop := $stop, step := $step : Range })
+  | `([ : $stop : $step ]) => `({ stop := $stop, step := $step : Range })
 
 end Range
 end Std
diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
index a9ba1b261e..c93768e10f 100644
--- a/src/Init/Data/Repr.lean
+++ b/src/Init/Data/Repr.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -13,167 +14,168 @@ open Sum Subtype Nat
 universes u v
 
 class HasRepr (α : Type u) :=
-(repr : α → String)
+  (repr : α → String)
 
 export HasRepr (repr)
 
 -- This instance is needed because `id` is not reducible
 instance {α : Type u} [HasRepr α] : HasRepr (id α) :=
-inferInstanceAs (HasRepr α)
+  inferInstanceAs (HasRepr α)
 
 instance : HasRepr Bool :=
-⟨fun b => cond b "true" "false"⟩
+  ⟨fun b => cond b "true" "false"⟩
 
 instance {α} [HasRepr α] : HasRepr (Id α) :=
-inferInstanceAs (HasRepr α)
+  inferInstanceAs (HasRepr α)
 
-instance {p : Prop} : HasRepr (Decidable p) :=
-⟨fun h => match h with
+instance {p : Prop} : HasRepr (Decidable p) := {
+  repr := fun h => match h with
   | Decidable.isTrue _  => "true"
-  | Decidable.isFalse _ => "false"⟩
+  | Decidable.isFalse _ => "false"
+}
 
 protected def List.reprAux {α : Type u} [HasRepr α] : Bool → List α → String
-| b,     []    => ""
-| true,  x::xs => repr x ++ List.reprAux false xs
-| false, x::xs => ", " ++ repr x ++ List.reprAux false xs
+  | b,     []    => ""
+  | true,  x::xs => repr x ++ List.reprAux false xs
+  | false, x::xs => ", " ++ repr x ++ List.reprAux false xs
 
 protected def List.repr {α : Type u} [HasRepr α] : List α → String
-| []    => "[]"
-| x::xs => "[" ++ List.reprAux true (x::xs) ++ "]"
+  | []    => "[]"
+  | x::xs => "[" ++ List.reprAux true (x::xs) ++ "]"
 
 instance {α : Type u} [HasRepr α] : HasRepr (List α) :=
-⟨List.repr⟩
+  ⟨List.repr⟩
 
 instance : HasRepr PUnit.{u+1} :=
-⟨fun u => "PUnit.unit"⟩
+  ⟨fun u => "PUnit.unit"⟩
 
 instance {α : Type u} [HasRepr α] : HasRepr (ULift.{v} α) :=
-⟨fun v => "ULift.up (" ++ repr v.1 ++ ")"⟩
+  ⟨fun v => "ULift.up (" ++ repr v.1 ++ ")"⟩
 
 instance : HasRepr Unit :=
-⟨fun u => "()"⟩
+  ⟨fun u => "()"⟩
 
 instance {α : Type u} [HasRepr α] : HasRepr (Option α) :=
-⟨fun o => match o with | none => "none" | (some a) => "(some " ++ repr a ++ ")"⟩
+  ⟨fun | none => "none" | (some a) => "(some " ++ repr a ++ ")"⟩
 
 instance {α : Type u} {β : Type v} [HasRepr α] [HasRepr β] : HasRepr (Sum α β) :=
-⟨fun s => match s with | (inl a) => "(inl " ++ repr a ++ ")" | (inr b) => "(inr " ++ repr b ++ ")"⟩
+  ⟨fun | (inl a) => "(inl " ++ repr a ++ ")" | (inr b) => "(inr " ++ repr b ++ ")"⟩
 
 instance {α : Type u} {β : Type v} [HasRepr α] [HasRepr β] : HasRepr (α × β) :=
-⟨fun ⟨a, b⟩ => "(" ++ repr a ++ ", " ++ repr b ++ ")"⟩
+  ⟨fun ⟨a, b⟩ => "(" ++ repr a ++ ", " ++ repr b ++ ")"⟩
 
 instance {α : Type u} {β : α → Type v} [HasRepr α] [s : ∀ x, HasRepr (β x)] : HasRepr (Sigma β) :=
-⟨fun ⟨a, b⟩ => "⟨"  ++ repr a ++ ", " ++ repr b ++ "⟩"⟩
+  ⟨fun ⟨a, b⟩ => "⟨"  ++ repr a ++ ", " ++ repr b ++ "⟩"⟩
 
 instance {α : Type u} {p : α → Prop} [HasRepr α] : HasRepr (Subtype p) :=
-⟨fun s => repr (val s)⟩
+  ⟨fun s => repr (val s)⟩
 
 namespace Nat
 
 def digitChar (n : Nat) : Char :=
-if n = 0 then '0' else
-if n = 1 then '1' else
-if n = 2 then '2' else
-if n = 3 then '3' else
-if n = 4 then '4' else
-if n = 5 then '5' else
-if n = 6 then '6' else
-if n = 7 then '7' else
-if n = 8 then '8' else
-if n = 9 then '9' else
-if n = 0xa then 'a' else
-if n = 0xb then 'b' else
-if n = 0xc then 'c' else
-if n = 0xd then 'd' else
-if n = 0xe then 'e' else
-if n = 0xf then 'f' else
-'*'
+  if n = 0 then '0' else
+  if n = 1 then '1' else
+  if n = 2 then '2' else
+  if n = 3 then '3' else
+  if n = 4 then '4' else
+  if n = 5 then '5' else
+  if n = 6 then '6' else
+  if n = 7 then '7' else
+  if n = 8 then '8' else
+  if n = 9 then '9' else
+  if n = 0xa then 'a' else
+  if n = 0xb then 'b' else
+  if n = 0xc then 'c' else
+  if n = 0xd then 'd' else
+  if n = 0xe then 'e' else
+  if n = 0xf then 'f' else
+  '*'
 
 def toDigitsCore (base : Nat) : Nat → Nat → List Char → List Char
-| 0,      n, ds => ds
-| fuel+1, n, ds =>
-  let d  := digitChar $ n % base;
-  let n' := n / base;
-  if n' = 0 then d::ds
-  else toDigitsCore fuel n' (d::ds)
+  | 0,      n, ds => ds
+  | fuel+1, n, ds =>
+    let d  := digitChar $ n % base;
+    let n' := n / base;
+    if n' = 0 then d::ds
+    else toDigitsCore base fuel n' (d::ds)
 
 def toDigits (base : Nat) (n : Nat) : List Char :=
-toDigitsCore base (n+1) n []
+  toDigitsCore base (n+1) n []
 
 protected def repr (n : Nat) : String :=
-(toDigits 10 n).asString
+  (toDigits 10 n).asString
 
 def superDigitChar (n : Nat) : Char :=
-if n = 0 then '⁰' else
-if n = 1 then '¹' else
-if n = 2 then '²' else
-if n = 3 then '³' else
-if n = 4 then '⁴' else
-if n = 5 then '⁵' else
-if n = 6 then '⁶' else
-if n = 7 then '⁷' else
-if n = 8 then '⁸' else
-if n = 9 then '⁹' else
-'*'
+  if n = 0 then '⁰' else
+  if n = 1 then '¹' else
+  if n = 2 then '²' else
+  if n = 3 then '³' else
+  if n = 4 then '⁴' else
+  if n = 5 then '⁵' else
+  if n = 6 then '⁶' else
+  if n = 7 then '⁷' else
+  if n = 8 then '⁸' else
+  if n = 9 then '⁹' else
+  '*'
 
 partial def toSuperDigitsAux : Nat → List Char → List Char
-| n, ds =>
-  let d  := superDigitChar $ n % 10;
-  let n' := n / 10;
-  if n' = 0 then d::ds
-  else toSuperDigitsAux n' (d::ds)
+  | n, ds =>
+    let d  := superDigitChar $ n % 10;
+    let n' := n / 10;
+    if n' = 0 then d::ds
+    else toSuperDigitsAux n' (d::ds)
 
 def toSuperDigits (n : Nat) : List Char :=
-toSuperDigitsAux n []
+  toSuperDigitsAux n []
 
 def toSuperscriptString (n : Nat) : String :=
-(toSuperDigits n).asString
+  (toSuperDigits n).asString
 
 end Nat
 
 instance : HasRepr Nat :=
-⟨Nat.repr⟩
+  ⟨Nat.repr⟩
 
 def hexDigitRepr (n : Nat) : String :=
-String.singleton $ Nat.digitChar n
+  String.singleton $ Nat.digitChar n
 
 def charToHex (c : Char) : String :=
-let n  := Char.toNat c;
-let d2 := n / 16;
-let d1 := n % 16;
-hexDigitRepr d2 ++ hexDigitRepr d1
+  let n  := Char.toNat c;
+  let d2 := n / 16;
+  let d1 := n % 16;
+  hexDigitRepr d2 ++ hexDigitRepr d1
 
 def Char.quoteCore (c : Char) : String :=
-if       c = '\n' then "\\n"
-else if  c = '\t' then "\\t"
-else if  c = '\\' then "\\\\"
-else if  c = '\"' then "\\\""
-else if  c.toNat <= 31 ∨ c = '\x7f' then "\\x" ++ charToHex c
-else String.singleton c
+  if       c = '\n' then "\\n"
+  else if  c = '\t' then "\\t"
+  else if  c = '\\' then "\\\\"
+  else if  c = '\"' then "\\\""
+  else if  c.toNat <= 31 ∨ c = '\x7f' then "\\x" ++ charToHex c
+  else String.singleton c
 
 instance : HasRepr Char :=
-⟨fun c => "'" ++ Char.quoteCore c ++ "'"⟩
+  ⟨fun c => "'" ++ Char.quoteCore c ++ "'"⟩
 
 def String.quote (s : String) : String :=
-if s.isEmpty = true then "\"\""
-else s.foldl (fun s c => s ++ c.quoteCore) "\"" ++ "\""
+  if s.isEmpty = true then "\"\""
+  else s.foldl (fun s c => s ++ c.quoteCore) "\"" ++ "\""
 
 instance : HasRepr String :=
-⟨String.quote⟩
+  ⟨String.quote⟩
 
 instance : HasRepr Substring :=
-⟨fun s => String.quote s.toString ++ ".toSubstring"⟩
+  ⟨fun s => String.quote s.toString ++ ".toSubstring"⟩
 
 instance : HasRepr String.Iterator :=
-⟨fun ⟨s, pos⟩ => "(String.Iterator.mk " ++ repr s ++ " " ++ repr pos ++ ")"⟩
+  ⟨fun ⟨s, pos⟩ => "(String.Iterator.mk " ++ repr s ++ " " ++ repr pos ++ ")"⟩
 
 instance (n : Nat) : HasRepr (Fin n) :=
-⟨fun f => repr (Fin.val f)⟩
+  ⟨fun f => repr (Fin.val f)⟩
 
 instance : HasRepr UInt16 := ⟨fun n => repr n.toNat⟩
 instance : HasRepr UInt32 := ⟨fun n => repr n.toNat⟩
 instance : HasRepr UInt64 := ⟨fun n => repr n.toNat⟩
 instance : HasRepr USize  := ⟨fun n => repr n.toNat⟩
 
-def Char.repr (c : Char) : String :=
-repr c
+protected def Char.repr (c : Char) : String :=
+  repr c
diff --git a/src/Init/Data/String.lean b/src/Init/Data/String.lean
index 43c77de907..c201a03d2a 100644
--- a/src/Init/Data/String.lean
+++ b/src/Init/Data/String.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
diff --git a/src/Init/Data/ToString.lean b/src/Init/Data/ToString.lean
index e5d7e81c79..4a854f4166 100644
--- a/src/Init/Data/ToString.lean
+++ b/src/Init/Data/ToString.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.