Lawful instances of MonadLift for the Lean monad stack.

instance instLawfulMonadLiftSTEST_batteries {σ ε : Type} : LawfulMonadLift (ST σ) (EST ε σ)

instance instLawfulMonadLiftBaseIOEIO_batteries {ε : Type} : LawfulMonadLift BaseIO (EIO ε)

EIO.adapt simp lemmas

@[simp]

theorem EIO.adapt_pure {ε₁ ε₂ α : Type} (f : ε₁ → ε₂) (a : α) : adapt f (pure a) = pure a

@[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

@[simp]

theorem StateRefT'.lift_pure {m : Type → Type} {α ω σ : Type} [Monad m] (a : α) : StateRefT'.lift (pure a) = pure a

@[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

instance instLawfulMonadLiftIOCoreM_batteries : LawfulMonadLift IO Lean.CoreM

instance instLawfulMonadLiftTEIOExceptionCommandElabM_batteries : LawfulMonadLiftT (EIO Lean.Exception) Lean.Elab.Command.CommandElabM

instance instLawfulMonadLiftTEIOExceptionCoreM_batteries : LawfulMonadLiftT (EIO Lean.Exception) Lean.CoreM

instance instLawfulMonadLiftTCoreMMetaM_batteries : LawfulMonadLiftT Lean.CoreM Lean.MetaM

instance instLawfulMonadLiftTMetaMTermElabM_batteries : LawfulMonadLiftT Lean.MetaM Lean.Elab.TermElabM

instance instLawfulMonadLiftTTermElabMTacticM_batteries : LawfulMonadLiftT Lean.Elab.TermElabM Lean.Elab.Tactic.TacticM