From 1e496fb32d79d5ee4c85fe8f2b2885f8318c3699 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 18 Aug 2020 13:26:14 -0700
Subject: [PATCH] feat: helper instance

---
 src/Init/Control/Reader.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean
index f1650bf165..f60bf75234 100644
--- a/src/Init/Control/Reader.lean
+++ b/src/Init/Control/Reader.lean
@@ -17,6 +17,9 @@ universes u v w
 def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
 ρ → m α
 
+instance ReaderT.inhabited (ρ : Type u) (m : Type u → Type v) (α : Type u) [Inhabited (m α)] : Inhabited (ReaderT ρ m α) :=
+⟨fun _ => arbitrary _⟩
+
 @[inline] def ReaderT.run {ρ : Type u} {m : Type u → Type v} {α : Type u} (x : ReaderT ρ m α) (r : ρ) : m α :=
 x r