Documentation

Init.Control.State

def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) :
Type (max u v)
Instances For
    @[inline]
    def StateT.run {σ : Type u} {m : Type u → Type v} {α : Type u} (x : StateT σ m α) (s : σ) :
    m (α × σ)
    Instances For
      @[inline]
      def StateT.run' {σ : Type u} {m : Type u → Type v} [Functor m] {α : Type u} (x : StateT σ m α) (s : σ) :
      m α
      Instances For
        @[reducible]
        def StateM (σ : Type u) (α : Type u) :
        Instances For
          instance instSubsingletonStateM {σ : Type u_1} {α : Type u_1} [Subsingleton σ] [Subsingleton α] :
          @[inline]
          def StateT.pure {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (a : α) :
          StateT σ m α
          Instances For
            @[inline]
            def StateT.bind {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} (x : StateT σ m α) (f : αStateT σ m β) :
            StateT σ m β
            Instances For
              @[inline]
              def StateT.map {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} (f : αβ) (x : StateT σ m α) :
              StateT σ m β
              Instances For
                @[always_inline]
                instance StateT.instMonadStateT {σ : Type u} {m : Type u → Type v} [Monad m] :
                Monad (StateT σ m)
                @[inline]
                def StateT.orElse {σ : Type u} {m : Type u → Type v} [Alternative m] {α : Type u} (x₁ : StateT σ m α) (x₂ : UnitStateT σ m α) :
                StateT σ m α
                Instances For
                  @[inline]
                  def StateT.failure {σ : Type u} {m : Type u → Type v} [Alternative m] {α : Type u} :
                  StateT σ m α
                  Instances For
                    instance StateT.instAlternativeStateT {σ : Type u} {m : Type u → Type v} [Monad m] [Alternative m] :
                    @[inline]
                    def StateT.get {σ : Type u} {m : Type u → Type v} [Monad m] :
                    StateT σ m σ
                    Instances For
                      @[inline]
                      def StateT.set {σ : Type u} {m : Type u → Type v} [Monad m] :
                      σStateT σ m PUnit
                      Instances For
                        @[inline]
                        def StateT.modifyGet {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (f : σα × σ) :
                        StateT σ m α
                        Instances For
                          @[inline]
                          def StateT.lift {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (t : m α) :
                          StateT σ m α
                          Instances For
                            instance StateT.instMonadLiftStateT {σ : Type u} {m : Type u → Type v} [Monad m] :
                            MonadLift m (StateT σ m)
                            @[always_inline]
                            instance StateT.instMonadFunctorStateT (σ : Type u_1) (m : Type u_1 → Type u_2) [Monad m] :
                            @[always_inline]
                            instance StateT.instMonadExceptOfStateT {σ : Type u} {m : Type u → Type v} [Monad m] (ε : Type u_1) [MonadExceptOf ε m] :
                            @[inline]
                            def ForM.forIn {m : Type u_1 → Type u_2} {β : Type u_1} {ρ : Type u_3} {α : Type u_4} [Monad m] [ForM (StateT β (ExceptT β m)) ρ α] (x : ρ) (b : β) (f : αβm (ForInStep β)) :
                            m β

                            Adapter to create a ForIn instance from a ForM instance

                            Instances For
                              instance instMonadStateOfStateT {σ : Type u} {m : Type u → Type v} [Monad m] :
                              @[always_inline]
                              instance StateT.monadControl (σ : Type u) (m : Type u → Type v) [Monad m] :
                              @[always_inline]
                              instance StateT.tryFinally {m : Type u → Type v} {σ : Type u} [MonadFinally m] [Monad m] :