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

fix: incorrect use of outParam

Browse source 
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
This commit is contained in:
Leonardo de Moura 2022-11-30 16:56:09 -08:00
parent dc937cb1f9
commit 8fbb866798
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/Util/Async.lean
View file

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