Construct LawfulMonad instances for the Lean monad stack.

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

Equations

• ⋯ = ⋯

instance instLawfulMonadBaseIO_batteries : LawfulMonad BaseIO

Equations

• instLawfulMonadBaseIO_batteries = ⋯

instance instLawfulMonadIO_batteries : LawfulMonad IO

Equations

• instLawfulMonadIO_batteries = ⋯

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

Equations

• ⋯ = ⋯

instance instLawfulMonadCoreM_batteries : LawfulMonad Lean.CoreM

Equations

• instLawfulMonadCoreM_batteries = ⋯

instance instLawfulMonadMetaM_batteries : LawfulMonad Lean.MetaM

Equations

• instLawfulMonadMetaM_batteries = ⋯

instance instLawfulMonadTermElabM_batteries : LawfulMonad Lean.Elab.TermElabM

Equations

• instLawfulMonadTermElabM_batteries = ⋯

instance instLawfulMonadTacticM_batteries : LawfulMonad Lean.Elab.Tactic.TacticM

Equations

• instLawfulMonadTacticM_batteries = ⋯

instance instLawfulMonadCommandElabM_batteries : LawfulMonad Lean.Elab.Command.CommandElabM

Equations

• instLawfulMonadCommandElabM_batteries = ⋯