# Documentation

## Init.System.ST

def EST (ε : Type) (σ : Type) :
Equations
Instances For
@[inline, reducible]
abbrev ST (σ : Type) :
Equations
Instances For
instance instMonadEST (ε : Type) (σ : Type) :
Equations
instance instMonadExceptOfEST (ε : Type) (σ : Type) :
Equations
instance instInhabitedEST {ε : Type} {σ : Type} {α : Type} [] :
Inhabited (EST ε σ α)
Equations
instance instMonadST (σ : Type) :
Equations
class STWorld (σ : ) (m : ) :
Instances
instance instSTWorld {σ : Type} {m : } {n : } [] [STWorld σ m] :
STWorld σ n
Equations
• instSTWorld = { }
instance instSTWorldEST {ε : Type} {σ : Type} :
STWorld σ (EST ε σ)
Equations
• instSTWorldEST = { }
@[noinline]
def runEST {ε : Type} {α : Type} (x : (σ : Type) → EST ε σ α) :
Except ε α
Equations
• = match with | => | =>
Instances For
@[noinline]
def runST {α : Type} (x : (σ : Type) → ST σ α) :
α
Equations
• = match with | => a | => nomatch ex
Instances For
@[always_inline]
instance instMonadLiftSTEST {ε : Type} {σ : Type} :
MonadLift (ST σ) (EST ε σ)
Equations
• One or more equations did not get rendered due to their size.
structure ST.Ref (σ : Type) (α : Type) :
• h :
Instances For
instance ST.instNonemptyRef {σ : Type} {α : Type} [s : ] :
Equations
• =
@[extern lean_st_mk_ref]
opaque ST.Prim.mkRef {σ : Type} {α : Type} (a : α) :
ST σ (ST.Ref σ α)
@[extern lean_st_ref_get]
opaque ST.Prim.Ref.get {σ : Type} {α : Type} (r : ST.Ref σ α) :
ST σ α
@[extern lean_st_ref_set]
opaque ST.Prim.Ref.set {σ : Type} {α : Type} (r : ST.Ref σ α) (a : α) :
@[extern lean_st_ref_swap]
opaque ST.Prim.Ref.swap {σ : Type} {α : Type} (r : ST.Ref σ α) (a : α) :
ST σ α
@[extern lean_st_ref_take]
unsafe opaque ST.Prim.Ref.take {σ : Type} {α : Type} (r : ST.Ref σ α) :
ST σ α
@[extern lean_st_ref_ptr_eq]
opaque ST.Prim.Ref.ptrEq {σ : Type} {α : Type} (r1 : ST.Ref σ α) (r2 : ST.Ref σ α) :
@[inline]
unsafe def ST.Prim.Ref.modifyUnsafe {σ : Type} {α : Type} (r : ST.Ref σ α) (f : αα) :
Equations
Instances For
@[inline]
unsafe def ST.Prim.Ref.modifyGetUnsafe {σ : Type} {α : Type} {β : Type} (r : ST.Ref σ α) (f : αβ × α) :
ST σ β
Equations
• = do let v ← match f v with | (b, a) => do pure b
Instances For
@[implemented_by ST.Prim.Ref.modifyUnsafe]
def ST.Prim.Ref.modify {σ : Type} {α : Type} (r : ST.Ref σ α) (f : αα) :
Equations
Instances For
@[implemented_by ST.Prim.Ref.modifyGetUnsafe]
def ST.Prim.Ref.modifyGet {σ : Type} {α : Type} {β : Type} (r : ST.Ref σ α) (f : αβ × α) :
ST σ β
Equations
• = do let v ← match f v with | (b, a) => do pure b
Instances For
@[inline]
def ST.mkRef {σ : Type} {m : } [MonadLiftT (ST σ) m] {α : Type} (a : α) :
m (ST.Ref σ α)
Equations
Instances For
@[inline]
def ST.Ref.get {σ : Type} {m : } [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) :
m α
Equations
Instances For
@[inline]
def ST.Ref.set {σ : Type} {m : } [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) (a : α) :
Equations
Instances For
@[inline]
def ST.Ref.swap {σ : Type} {m : } [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) (a : α) :
m α
Equations
Instances For
@[inline]
unsafe def ST.Ref.take {σ : Type} {m : } [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) :
m α
Equations
Instances For
@[inline]
def ST.Ref.ptrEq {σ : Type} {m : } [MonadLiftT (ST σ) m] {α : Type} (r1 : ST.Ref σ α) (r2 : ST.Ref σ α) :
Equations
Instances For
@[inline]
def ST.Ref.modify {σ : Type} {m : } [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) (f : αα) :
Equations
Instances For
@[inline]
def ST.Ref.modifyGet {σ : Type} {m : } [MonadLiftT (ST σ) m] {α : Type} {β : Type} (r : ST.Ref σ α) (f : αβ × α) :
m β
Equations
Instances For
def ST.Ref.toMonadStateOf {σ : Type} {m : } [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) :
Equations
• = { get := , set := , modifyGet := fun {α_1 : Type} => }
Instances For