Documentation

Init.Control.State

def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) :
Type (max u v)
Equations
Instances For
    @[inline]
    def StateT.run {σ : Type u} {m : Type u → Type v} {α : Type u} (x : StateT σ m α) (s : σ) :
    m (α × σ)
    Equations
    Instances For
      @[inline]
      def StateT.run' {σ : Type u} {m : Type u → Type v} [Functor m] {α : Type u} (x : StateT σ m α) (s : σ) :
      m α
      Equations
      Instances For
        @[reducible]
        def StateM (σ : Type u) (α : Type u) :
        Equations
        Instances For
          instance instSubsingletonStateM {σ : Type u_1} {α : Type u_1} [Subsingleton σ] [Subsingleton α] :
          Equations
          @[inline]
          def StateT.pure {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (a : α) :
          StateT σ m α
          Equations
          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 β
            Equations
            • StateT.bind x f s = do let __discr ← x s match __discr with | (a, s) => f a s
            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 β
              Equations
              • StateT.map f x s = do let __discr ← x s match __discr with | (a, s) => pure (f a, s)
              Instances For
                @[always_inline]
                instance StateT.instMonadStateT {σ : Type u} {m : Type u → Type v} [Monad m] :
                Monad (StateT σ m)
                Equations
                • StateT.instMonadStateT = Monad.mk
                @[inline]
                def StateT.orElse {σ : Type u} {m : Type u → Type v} [Alternative m] {α : Type u} (x₁ : StateT σ m α) (x₂ : UnitStateT σ m α) :
                StateT σ m α
                Equations
                Instances For
                  @[inline]
                  def StateT.failure {σ : Type u} {m : Type u → Type v} [Alternative m] {α : Type u} :
                  StateT σ m α
                  Equations
                  Instances For
                    instance StateT.instAlternativeStateT {σ : Type u} {m : Type u → Type v} [Monad m] [Alternative m] :
                    Equations
                    • StateT.instAlternativeStateT = Alternative.mk (fun {α : Type u} => StateT.failure) fun {α : Type u} => StateT.orElse
                    @[inline]
                    def StateT.get {σ : Type u} {m : Type u → Type v} [Monad m] :
                    StateT σ m σ
                    Equations
                    Instances For
                      @[inline]
                      def StateT.set {σ : Type u} {m : Type u → Type v} [Monad m] :
                      σStateT σ m PUnit
                      Equations
                      Instances For
                        @[inline]
                        def StateT.modifyGet {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (f : σα × σ) :
                        StateT σ m α
                        Equations
                        Instances For
                          @[inline]
                          def StateT.lift {σ : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (t : m α) :
                          StateT σ m α
                          Equations
                          Instances For
                            instance StateT.instMonadLiftStateT {σ : Type u} {m : Type u → Type v} [Monad m] :
                            MonadLift m (StateT σ m)
                            Equations
                            • StateT.instMonadLiftStateT = { monadLift := fun {α : Type u} => StateT.lift }
                            @[always_inline]
                            instance StateT.instMonadFunctorStateT (σ : Type u_1) (m : Type u_1 → Type u_2) [Monad m] :
                            Equations
                            @[always_inline]
                            instance StateT.instMonadExceptOfStateT {σ : Type u} {m : Type u → Type v} [Monad m] (ε : Type u_1) [MonadExceptOf ε m] :
                            Equations
                            • One or more equations did not get rendered due to their size.
                            @[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

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              instance instMonadStateOfStateT {σ : Type u} {m : Type u → Type v} [Monad m] :
                              Equations
                              • instMonadStateOfStateT = { get := StateT.get, set := StateT.set, modifyGet := fun {α : Type u} => StateT.modifyGet }
                              @[always_inline]
                              instance StateT.monadControl (σ : Type u) (m : Type u → Type v) [Monad m] :
                              Equations
                              • One or more equations did not get rendered due to their size.
                              @[always_inline]
                              instance StateT.tryFinally {m : Type u → Type v} {σ : Type u} [MonadFinally m] [Monad m] :
                              Equations
                              • One or more equations did not get rendered due to their size.