max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: remove Monad Task instance (for now)

Browse source
This commit is contained in:
tydeu 2021-07-14 14:53:52 -04:00
parent e040804678
commit 31fa37dbfe
1 changed files with 1 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
Lake/BuildTask.lean
View file

@ -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