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

refactor: generalize Await signature a little

Browse source
This commit is contained in:
tydeu 2021-10-27 12:19:02 -04:00
parent b0991cf96b
commit 781672e935
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake/Async.lean
View file

@ -16,7 +16,7 @@ class Async (m : Type u → Type v) (n : outParam $ Type u → Type u) where
export Async (async)
class Await (n : Type u → Type u) (m : Type u → Type v) where
class Await (n : Type u → Type v) (m : Type u → Type w) where
/- Wait for an asynchronous task to finish. -/
await : n α → m α