From 31fa37dbfefc7b726718fe81f257ab6e418743bb Mon Sep 17 00:00:00 2001 From: tydeu Date: Wed, 14 Jul 2021 14:53:52 -0400 Subject: [PATCH] refactor: remove `Monad Task` instance (for now) --- Lake/BuildTask.lean | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/Lake/BuildTask.lean b/Lake/BuildTask.lean index 5e55d90cb1..0451022306 100644 --- a/Lake/BuildTask.lean +++ b/Lake/BuildTask.lean @@ -6,11 +6,6 @@ Authors: Mac Malone namespace Lake -instance : Monad Task where - map := Task.map - pure := Task.pure - bind := Task.bind - abbrev ETask ε α := ExceptT ε Task α abbrev IOTask α := ETask IO.Error α @@ -33,7 +28,7 @@ def BuildTask := IOTask PUnit namespace BuildTask def nop : BuildTask := - pure () + Task.pure (Except.ok ()) def spawn (act : IO PUnit) (prio := Task.Priority.dedicated) : IO BuildTask := IO.asTask act prio