Documentation

Batteries.Lean.LawfulMonadLift

Lawful instances of MonadLift for the Lean monad stack. #

source
instance instLawfulMonadLiftBaseIOEIO {ε : Type} :
LawfulMonadLift BaseIO (EIO ε)
source
instance instLawfulMonadLiftSTEST {σ ε : Type} :
LawfulMonadLift (ST σ) (EST ε σ)
source
instance instLawfulMonadLiftIOCoreM :
LawfulMonadLift IO Lean.CoreM
source
instance instLawfulMonadLiftTEIOExceptionCommandElabM :
LawfulMonadLiftT (EIO Lean.Exception) Lean.Elab.Command.CommandElabM
source
instance instLawfulMonadLiftTEIOExceptionCoreM :
LawfulMonadLiftT (EIO Lean.Exception) Lean.CoreM
source
instance instLawfulMonadLiftTCoreMMetaM :
LawfulMonadLiftT Lean.CoreM Lean.MetaM
source
instance instLawfulMonadLiftTMetaMTermElabM :
LawfulMonadLiftT Lean.MetaM Lean.Elab.TermElabM
source
instance instLawfulMonadLiftTTermElabMTacticM :
LawfulMonadLiftT Lean.Elab.TermElabM Lean.Elab.Tactic.TacticM