Zulip Chat Archive
Stream: general
Topic: Dependent state monad
Konstantin Weitz (Jul 12 2025 at 15:41):
I have this dependent state monad, how do I express this in Lean with the standard library?
(a:BusConfig) -> (b:BusConfig) × Factory n (busInterface b) s (busInterface a)
Aaron Liu (Jul 12 2025 at 15:49):
What's the signature of the monadic bind?
Henrik Böving (Jul 12 2025 at 15:50):
This doesn't really exist in the stdlib right now unfortunately.
Last updated: Dec 20 2025 at 21:32 UTC