Construct MonadSatisfying instances for the Lean monad stack.

def instMonadSatisfyingEIO {ε : Type} : MonadSatisfying (EIO ε)

Equations

• Eq instMonadSatisfyingEIO (inferInstanceAs (MonadSatisfying (EStateM ε IO.RealWorld)))

def instMonadSatisfyingBaseIO : MonadSatisfying BaseIO

Equations

• Eq instMonadSatisfyingBaseIO (inferInstanceAs (MonadSatisfying (EIO Empty)))

def instMonadSatisfyingIO : MonadSatisfying IO

Equations

• Eq instMonadSatisfyingIO (inferInstanceAs (MonadSatisfying (EIO IO.Error)))

def instMonadSatisfyingEST {ε σ : Type} : MonadSatisfying (EST ε σ)

Equations

• Eq instMonadSatisfyingEST (inferInstanceAs (MonadSatisfying (EStateM ε σ)))

def instMonadSatisfyingCoreM : MonadSatisfying Lean.Core.CoreM

Equations

• Eq instMonadSatisfyingCoreM (inferInstanceAs (MonadSatisfying (ReaderT Lean.Core.Context (StateRefT' IO.RealWorld Lean.Core.State (EIO Lean.Exception)))))

def instMonadSatisfyingMetaM : MonadSatisfying Lean.Meta.MetaM

Equations

• Eq instMonadSatisfyingMetaM (inferInstanceAs (MonadSatisfying (ReaderT Lean.Meta.Context (StateRefT' IO.RealWorld Lean.Meta.State Lean.Core.CoreM))))

def instMonadSatisfyingTermElabM : MonadSatisfying Lean.Elab.Term.TermElabM

Equations

• Eq instMonadSatisfyingTermElabM (inferInstanceAs (MonadSatisfying (ReaderT Lean.Elab.Term.Context (StateRefT' IO.RealWorld Lean.Elab.Term.State Lean.Meta.MetaM))))

def instMonadSatisfyingTacticM : MonadSatisfying Lean.Elab.Tactic.TacticM

Equations

• Eq instMonadSatisfyingTacticM (inferInstanceAs (MonadSatisfying (ReaderT Lean.Elab.Tactic.Context (StateRefT' IO.RealWorld Lean.Elab.Tactic.State Lean.Elab.Term.TermElabM))))

def instMonadSatisfyingCommandElabM : MonadSatisfying Lean.Elab.Command.CommandElabM

Equations

• Eq instMonadSatisfyingCommandElabM (inferInstanceAs (MonadSatisfying (ReaderT Lean.Elab.Command.Context (StateRefT' IO.RealWorld Lean.Elab.Command.State (EIO Lean.Exception)))))