Is there any plan for asynchronous paradigm?

Stream: lean4

[Qiu]

Current uses of Task and IO.Promise are very messy in the reuse system. Maybe we can extend do-notation to support some kind of asynchronous paradigm?

[Markus Himmel]

Yes, this is on the horizon, see lean4#8003.