From b80775df6faa9aac24ba4e574af3839c3d791e19 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Wed, 20 Jul 2022 10:32:31 +0200
Subject: [PATCH] chore: add nonempty instance for monads

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

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 9ae195c2ee..8f9a35a908 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2663,6 +2663,9 @@ instance {α : Type u} {m : Type u → Type v} [Monad m] : Inhabited (α → m 
 instance {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabited (m α) where
   default := pure default
 
+instance [Monad m] : [Nonempty α] → Nonempty (m α)
+  | ⟨x⟩ => ⟨pure x⟩
+
 /-- A fusion of Haskell's `sequence` and `map`. Used in syntax quotations. -/
 def Array.sequenceMap {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m β) : m (Array β) :=
   let rec loop (i : Nat) (j : Nat) (bs : Array β) : m (Array β) :=