Documentation

Batteries.Lean.SatisfiesM

Construct `MonadSatisfying` instances for the Lean monad stack. #

instance instMonadSatisfyingEIO {ε : Type} :

MonadSatisfying (EIO ε)

Equations

instMonadSatisfyingEIO = inferInstanceAs (MonadSatisfying (EStateM ε IO.RealWorld))

instance instMonadSatisfyingBaseIO :

MonadSatisfying BaseIO

Equations

instMonadSatisfyingBaseIO = inferInstanceAs (MonadSatisfying (EIO Empty))

instance instMonadSatisfyingIO :

MonadSatisfying IO

Equations

instMonadSatisfyingIO = inferInstanceAs (MonadSatisfying (EIO IO.Error))

instance instMonadSatisfyingEST {ε σ : Type} :

MonadSatisfying (EST ε σ)

Equations

instMonadSatisfyingEST = inferInstanceAs (MonadSatisfying (EStateM ε σ))

instance instMonadSatisfyingCoreM :

MonadSatisfying Lean.CoreM

Equations

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

instance instMonadSatisfyingMetaM :

MonadSatisfying Lean.MetaM

Equations

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

instance instMonadSatisfyingTermElabM :

MonadSatisfying Lean.Elab.TermElabM

Equations

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

instance instMonadSatisfyingTacticM :

MonadSatisfying Lean.Elab.Tactic.TacticM

Equations

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

instance instMonadSatisfyingCommandElabM :

MonadSatisfying Lean.Elab.Command.CommandElabM

Equations

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