From 781672e935f70a435ebac56778c8985dff205a56 Mon Sep 17 00:00:00 2001 From: tydeu Date: Wed, 27 Oct 2021 12:19:02 -0400 Subject: [PATCH] refactor: generalize `Await` signature a little --- Lake/Async.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Lake/Async.lean b/Lake/Async.lean index 49812a85d8..ff1d425157 100644 --- a/Lake/Async.lean +++ b/Lake/Async.lean @@ -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 α