Documentation

Batteries.Lean.LawfulMonadLift

Lawful instances of MonadLift for the Lean monad stack. #

source
instance instLawfulMonadLiftSTEST_batteries {σ ε : Type} :
LawfulMonadLift (ST σ) (EST ε σ)
source
instance instLawfulMonadLiftBaseIOEIO_batteries {ε : Type} :
LawfulMonadLift BaseIO (EIO ε)

EIO.adapt simp lemmas #

source
@[simp]
theorem EIO.adapt_pure {ε₁ ε₂ α : Type} (f : ε₁ → ε₂) (a : α) :
adapt f (pure a) = pure a
source
@[simp]
theorem EIO.adapt_bind {ε₁ ε₂ α β : Type} (f : ε₁ → ε₂) (ma : EIO ε₁ α) (g : α → EIO ε₁ β) :
adapt f (ma >>= g) = do let a ← adapt f ma adapt f (g a)

StateRefT'.lift simp lemmas #

source
@[simp]
theorem StateRefT'.lift_pure {m : Type → Type} {α ω σ : Type} [Monad m] (a : α) :
StateRefT'.lift (pure a) = pure a
source
@[simp]
theorem StateRefT'.lift_bind {m : Type → Type} {α β ω σ : Type} [Monad m] (ma : m α) (f : α → m β) :
StateRefT'.lift (ma >>= f) = do let a ← StateRefT'.lift ma StateRefT'.lift (f a)

LawfulMonadLift IO CoreM #

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