Documentation

Init.Control.StateRef

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

@[inline]
def StateRefT'.run {ω σ : 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)
@[inline]
def StateRefT'.run' {ω σ : 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
@[inline]
def StateRefT'.lift {ω σ : Type} {m : TypeType} {α : Type} (x : m α) :
StateRefT' ω σ m α
Equations
instance StateRefT'.instMonad {ω σ : Type} {m : TypeType} [Monad m] :
Monad (StateRefT' ω σ m)
Equations
instance StateRefT'.instMonadLift {ω σ : Type} {m : TypeType} :
MonadLift m (StateRefT' ω σ m)
Equations
@[inline]
def StateRefT'.get {ω σ : Type} {m : TypeType} [MonadLiftT (ST ω) m] :
StateRefT' ω σ m σ
Equations
@[inline]
def StateRefT'.set {ω σ : Type} {m : TypeType} [MonadLiftT (ST ω) m] (s : σ) :
Equations
@[inline]
def StateRefT'.modifyGet {ω σ : Type} {m : TypeType} {α : Type} [MonadLiftT (ST ω) m] (f : σα × σ) :
StateRefT' ω σ m α
Equations
@[always_inline]
instance StateRefT'.instMonadExceptOf {ω σ : Type} {m : TypeType} (ε : Type u_1) [MonadExceptOf ε m] :
Equations
  • One or more equations did not get rendered due to their size.