Construct LawfulMonad instances for the Lean monad stack.

instance instLawfulMonadST_batteries {σ : Type} : LawfulMonad (ST σ)

instance instLawfulMonadEST_batteries {ε σ : Type} : LawfulMonad (EST ε σ)

instance instLawfulMonadEIO_batteries {ε : Type} : LawfulMonad (EIO ε)

instance instLawfulMonadBaseIO_batteries : LawfulMonad BaseIO

instance instLawfulMonadIO_batteries : LawfulMonad IO

instance instLawfulMonadCoreM_batteries : LawfulMonad Lean.CoreM

instance instLawfulMonadMetaM_batteries : LawfulMonad Lean.MetaM

instance instLawfulMonadTermElabM_batteries : LawfulMonad Lean.Elab.TermElabM

instance instLawfulMonadTacticM_batteries : LawfulMonad Lean.Elab.Tactic.TacticM

instance instLawfulMonadCommandElabM_batteries : LawfulMonad Lean.Elab.Command.CommandElabM