effectful transition systems in do-notation

• do-notation - theory of symmetric monoidal categories