WriterT Monad

Stream: lean4

[lorã]

Hello, I am looking for a built-in implementation similar to the WriterT monad. I suspect it might exist under a different name, but I have been unable to locate it. What I should use instead? (I am also prepared to implement it myself if a suitable built-in option is not available)
~ Thank you for your time.

[Aaron Liu]

what do you mean by "builtin"?

[lorã]

Ty for the question! Ideally, I'm looking for a solution in the standard library. However, any stable, existing implementation would also be sufficient for my needs.

[Eric Wieser]

So docs#WriterT ?

[lorã]

oh, its in mathlib! Thank u! I was not expecting that there, sorry