Documentation

Batteries.Lean.SatisfiesM

Construct MonadSatisfying instances for the Lean monad stack. #

source
instance instMonadSatisfyingEIO {ε : Type} :
MonadSatisfying (EIO ε)
Equations
    source
    instance instMonadSatisfyingBaseIO :
    MonadSatisfying BaseIO
    Equations
      source
      instance instMonadSatisfyingIO :
      MonadSatisfying IO
      Equations
        source
        instance instMonadSatisfyingEST {ε σ : Type} :
        MonadSatisfying (EST ε σ)
        Equations
          source
          instance instMonadSatisfyingCoreM :
          MonadSatisfying Lean.CoreM
          Equations
            source
            instance instMonadSatisfyingMetaM :
            MonadSatisfying Lean.MetaM
            Equations
              source
              instance instMonadSatisfyingTermElabM :
              MonadSatisfying Lean.Elab.TermElabM
              Equations
                source
                instance instMonadSatisfyingTacticM :
                MonadSatisfying Lean.Elab.Tactic.TacticM
                Equations
                  source
                  instance instMonadSatisfyingCommandElabM :
                  MonadSatisfying Lean.Elab.Command.CommandElabM
                  Equations