https://lean-lang.org/doc/reference/latest/Functors___-Monads-and--do--Notation/Lifting-Monads/#MonadLift___mk Example Lifting Transformed Monads ``` def incrBy (n : Nat) : StateM Nat Unit := modify (def incrOrFail : ReaderT Nat (ExceptT String (StateM Nat)) Unit := do if (← read) > 5 then throw "Too much!" incrBy (← read) ```