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

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

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index c5daf7ed94..fee7d34327 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -366,6 +366,9 @@ structure Task (α : Type u) : Type u where
 attribute [extern "lean_task_pure"] Task.pure
 attribute [extern "lean_task_get_own"] Task.get
 
+instance : [Nonempty α] → Nonempty (Task α)
+  | ⟨x⟩ => ⟨.pure x⟩
+
 namespace Task
 /-- Task priority. Tasks with higher priority will always be scheduled before ones with lower priority. -/
 abbrev Priority := Nat