From 8fbb866798e4a4b597edda213ca737561951bca7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 30 Nov 2022 16:56:09 -0800 Subject: [PATCH] fix: incorrect use of `outParam` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We have ``` class BindAsync (n : Type u → Type v) (k : outParam $ Type u → Type u) instance : BindAsync BaseIO (EIOTask ε) instance : BindAsync BaseIO OptionIOTask instance [BindAsync n k] [Pure n] [Pure k] : BindAsync n (ExceptT ε k) instance [BindAsync n k] [Pure n] [Pure k] : BindAsync n (OptionT k) ``` See discussion at: https://leanprover.zulipchat.com/#narrow/stream/147302-lean4-maintainers/topic/Increasing.20.60Expr.2Ehash.60.20to.2064.20bits/near/313183466 --- Lake/Util/Async.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Lake/Util/Async.lean b/Lake/Util/Async.lean index 3664a846c9..1740a632de 100644 --- a/Lake/Util/Async.lean +++ b/Lake/Util/Async.lean @@ -105,7 +105,7 @@ class BindSync (m : Type u → Type v) (n : outParam $ Type u' → Type w) (k : export BindSync (bindSync) -class BindAsync (n : Type u → Type v) (k : outParam $ Type u → Type u) where +class BindAsync (n : Type u → Type v) (k : Type u → Type u) where /-- Perform a asynchronous task after another (a)synchronous task completes successfully. -/ bindAsync {α β : Type u} : k α → (α → n (k β)) → n (k β)