Should `Thunk` have a `Monad` instance?

Stream: lean4

[Vilim Lendvaj]

It already has map, pure and bind functions, seems pretty straightforward. LawfulMonad is also just by intros; rfl for everything.

[Asei Inoue]

interesting

[František Silváši 🦉]

#lean4 > Why isn't Thunk a Monad?

[Vilim Lendvaj]

If I'm reading that thread right, it can be done now?

[Eric Wieser]

I think best to post a remark along those lines in the original thread