diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean
index 3d61920369..f2d535c62a 100644
--- a/src/Init/Control/Option.lean
+++ b/src/Init/Control/Option.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.
@@ -17,53 +18,48 @@ m (Option α)
 x
 
 namespace OptionT
-  variables {m : Type u → Type v} [Monad m] {α β : Type u}
+variables {m : Type u → Type v} [Monad m] {α β : Type u}
 
-  @[inline] protected def bind (ma : OptionT m α) (f : α → OptionT m β) : OptionT m β :=
-  (do {
-    a? ← ma;
-    match a? with
-    | some a => f a
-    | none   => pure none
-  } : m (Option β))
+@[inline] protected def bind (x : OptionT m α) (f : α → OptionT m β) : OptionT m β := id (α := m (Option β)) do
+  match (← x) with
+  | some a => f a
+  | none   => pure none
 
-  @[inline] protected def pure (a : α) : OptionT m α :=
-  (pure (some a) : m (Option α))
+@[inline] protected def pure (a : α) : OptionT m α := id (α := m (Option α)) do
+  pure (some a)
 
-  instance : Monad (OptionT m) :=
-  { pure := @OptionT.pure _ _, bind := @OptionT.bind _ _ }
+instance : Monad (OptionT m) := {
+  pure := OptionT.pure,
+  bind := OptionT.bind
+}
 
-  @[inline] protected def orelse (ma : OptionT m α) (mb : OptionT m α) : OptionT m α :=
-  (do { a? ← ma;
-        match a? with
-        | some a => pure (some a)
-        | _      => mb } : m (Option α))
+@[inline] protected def orelse (x : OptionT m α) (y : OptionT m α) : OptionT m α := id (α := m (Option α)) do
+  match (← x) with
+  | some a => pure (some a)
+  | _      => y
 
-  @[inline] protected def fail : OptionT m α :=
-  (pure none : m (Option α))
+@[inline] protected def fail : OptionT m α := id (α := m (Option α)) do
+  pure none
 
-  instance : Alternative (OptionT m) :=
-  { OptionT.Monad with
-    failure := @OptionT.fail m _,
-    orelse  := @OptionT.orelse m _ }
+instance : Alternative (OptionT m) := {
+  failure := OptionT.fail,
+  orelse  := OptionT.orelse
+}
 
-  @[inline] protected def lift (ma : m α) : OptionT m α :=
-  (some <$> ma : m (Option α))
+@[inline] protected def lift (x : m α) : OptionT m α := id (α := m (Option α)) do
+  return some (← x)
 
-  instance : MonadLift m (OptionT m) :=
-  ⟨@OptionT.lift _ _⟩
+instance : MonadLift m (OptionT m) := ⟨OptionT.lift⟩
 
-  @[inline] protected def monadMap {m'} [Monad m'] {α} (f : ∀ {α}, m α → m' α) : OptionT m α → OptionT m' α :=
-  fun x => f x
+instance : MonadFunctor m (OptionT m) := ⟨fun f x => f x⟩
 
-  instance : MonadFunctor m (OptionT m) :=
-  ⟨fun α => OptionT.monadMap⟩
+@[inline] protected def «catch» (x : OptionT m α) (handle : Unit → OptionT m α) : OptionT m α := id (α := m (Option α)) do
+let some a ← x | handle ()
+pure a
 
-  @[inline] protected def catch (ma : OptionT m α) (handle : Unit → OptionT m α) : OptionT m α :=
-  (do { some a ← ma | (handle ());
-        pure a } : m (Option α))
-
-  instance : MonadExceptOf Unit (OptionT m) :=
-  { throw := fun _ _ => OptionT.fail, catch := @OptionT.catch _ _ }
+instance : MonadExceptOf Unit (OptionT m) := {
+  throw   := fun _ => OptionT.fail,
+  «catch» := OptionT.«catch»
+}
 
 end OptionT