Documentation

Init.Control.StateRef

def StateRefT' (ω : Type) (σ : Type) (m : TypeType) (α : Type) :
Equations
Instances For

    Recall that StateRefT is a macro that infers ω from the m.

    @[inline]
    def StateRefT'.run {ω : Type} {σ : Type} {m : TypeType} [Monad m] [MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) :
    m (α × σ)
    Equations
    • x.run s = do let refST.mkRef s let ax ref let sref.get pure (a, s)
    Instances For
      @[inline]
      def StateRefT'.run' {ω : Type} {σ : Type} {m : TypeType} [Monad m] [MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) :
      m α
      Equations
      • x.run' s = do let __discrx.run s match __discr with | (a, snd) => pure a
      Instances For
        @[inline]
        def StateRefT'.lift {ω : Type} {σ : Type} {m : TypeType} {α : Type} (x : m α) :
        StateRefT' ω σ m α
        Equations
        Instances For
          instance StateRefT'.instMonad {ω : Type} {σ : Type} {m : TypeType} [Monad m] :
          Monad (StateRefT' ω σ m)
          Equations
          instance StateRefT'.instMonadLift {ω : Type} {σ : Type} {m : TypeType} :
          MonadLift m (StateRefT' ω σ m)
          Equations
          • StateRefT'.instMonadLift = { monadLift := fun {α : Type} => StateRefT'.lift }
          instance StateRefT'.instAlternativeOfMonad {ω : Type} {σ : Type} {m : TypeType} [Alternative m] [Monad m] :
          Equations
          @[inline]
          def StateRefT'.get {ω : Type} {σ : Type} {m : TypeType} [MonadLiftT (ST ω) m] :
          StateRefT' ω σ m σ
          Equations
          Instances For
            @[inline]
            def StateRefT'.set {ω : Type} {σ : Type} {m : TypeType} [MonadLiftT (ST ω) m] (s : σ) :
            Equations
            Instances For
              @[inline]
              def StateRefT'.modifyGet {ω : Type} {σ : Type} {m : TypeType} {α : Type} [MonadLiftT (ST ω) m] (f : σα × σ) :
              StateRefT' ω σ m α
              Equations
              Instances For
                instance StateRefT'.instMonadStateOfOfMonadLiftTST {ω : Type} {σ : Type} {m : TypeType} [MonadLiftT (ST ω) m] :
                Equations
                • StateRefT'.instMonadStateOfOfMonadLiftTST = { get := StateRefT'.get, set := StateRefT'.set, modifyGet := fun {α : Type} => StateRefT'.modifyGet }
                @[always_inline]
                instance StateRefT'.instMonadExceptOf {ω : Type} {σ : Type} {m : TypeType} (ε : Type u_1) [MonadExceptOf ε m] :
                Equations
                • One or more equations did not get rendered due to their size.
                instance instMonadFinallyStateRefT' {m : TypeType} {ω : Type} {σ : Type} [MonadFinally m] :
                Equations