Documentation

Batteries.Lean.LawfulMonadLift

Lawful instances of MonadLift for the Lean monad stack. #

source
instance instLawfulMonadLiftBaseIOEIO_batteries {ε : Type} :
LawfulMonadLift BaseIO (EIO ε)
source
instance instLawfulMonadLiftSTEST_batteries {σ ε : Type} :
LawfulMonadLift (ST σ) (EST ε σ)
source
instance instLawfulMonadLiftIOCoreM_batteries :
LawfulMonadLift IO Lean.CoreM
source
instance instLawfulMonadLiftTEIOExceptionCommandElabM_batteries :
LawfulMonadLiftT (EIO Lean.Exception) Lean.Elab.Command.CommandElabM
source
instance instLawfulMonadLiftTEIOExceptionCoreM_batteries :
LawfulMonadLiftT (EIO Lean.Exception) Lean.CoreM
source
instance instLawfulMonadLiftTCoreMMetaM_batteries :
LawfulMonadLiftT Lean.CoreM Lean.MetaM
source
instance instLawfulMonadLiftTMetaMTermElabM_batteries :
LawfulMonadLiftT Lean.MetaM Lean.Elab.TermElabM
source
instance instLawfulMonadLiftTTermElabMTacticM_batteries :
LawfulMonadLiftT Lean.Elab.TermElabM Lean.Elab.Tactic.TacticM