Documentation

Batteries.Lean.LawfulMonad

Construct LawfulMonad instances for the Lean monad stack. #

source
instance instLawfulMonadEIO_batteries {ε : Type} :
LawfulMonad (EIO ε)
source
instance instLawfulMonadBaseIO_batteries :
LawfulMonad BaseIO
source
instance instLawfulMonadIO_batteries :
LawfulMonad IO
source
instance instLawfulMonadEST_batteries {ε σ : Type} :
LawfulMonad (EST ε σ)
source
instance instLawfulMonadCoreM_batteries :
LawfulMonad Lean.CoreM
source
instance instLawfulMonadMetaM_batteries :
LawfulMonad Lean.MetaM
source
instance instLawfulMonadTermElabM_batteries :
LawfulMonad Lean.Elab.TermElabM
source
instance instLawfulMonadTacticM_batteries :
LawfulMonad Lean.Elab.Tactic.TacticM
source
instance instLawfulMonadCommandElabM_batteries :
LawfulMonad Lean.Elab.Command.CommandElabM