Zulip Chat Archive

Stream: lean4

Topic: Is there any plan for asynchronous paradigm?

Jianqiu Zhao (Jun 02 2025 at 12:18):

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 (Jun 02 2025 at 12:25):

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

Last updated: Feb 28 2026 at 14:05 UTC