Documentation

Init.System.ST

source
noncomputable def EST (ε : Type) (σ : Type) :
Type → Type
Equations
source
@[inline]
abbrev ST (σ : Type) :
Type → Type
Equations
source
instance instMonadEST (ε : Type) (σ : Type) :
Monad (EST ε σ)
Equations
source
instance instMonadExceptOfEST (ε : Type) (σ : Type) :
MonadExceptOf ε (EST ε σ)
Equations
source
instance instInhabitedEST {ε : Type} {σ : Type} {α : Type} [inst : Inhabited ε] :
Inhabited (EST ε σ α)
Equations
source
instance instMonadST (σ : Type) :
Monad (ST σ)
Equations
source
class STWorld (σ : outParam Type) (m : Type → Type) :
Type
Instances
source
instance instSTWorld {σ : outParam Type} {m : Type → Type} {n : Type → Type} [inst : MonadLift m n] [inst : STWorld σ m] :
STWorld σ n
Equations
  • instSTWorld = { }
source
instance instSTWorldEST {ε : Type} {σ : outParam Type} :
STWorld σ (EST ε σ)
Equations
  • instSTWorldEST = { }
source
@[noinline, nospecialize]
def runEST {ε : Type} {α : Type} (x : (σ : Type) → EST ε σ α) :
Except ε α
Equations
source
@[noinline, nospecialize]
def runST {α : Type} (x : (σ : Type) → ST σ α) :
α
Equations
source
instance instMonadLiftSTEST {ε : Type} {σ : Type} :
MonadLift (ST σ) (EST ε σ)
Equations
source
constant ST.RefPointed :
NonemptyType
source
structure ST.Ref (σ : Type) (α : Type) :
Type
source
noncomputable instance ST.instNonemptyRef {σ : Type} {α : Type} [s : Nonempty α] :
Nonempty (ST.Ref σ α)
Equations
source
@[extern lean_st_mk_ref]
constant ST.Prim.mkRef {σ : Type} {α : Type} (a : α) :
ST σ (ST.Ref σ α)
source
@[extern lean_st_ref_get]
constant ST.Prim.Ref.get {σ : Type} {α : Type} (r : ST.Ref σ α) :
ST σ α
source
@[extern lean_st_ref_set]
constant ST.Prim.Ref.set {σ : Type} {α : Type} (r : ST.Ref σ α) (a : α) :
ST σ Unit
source
@[extern lean_st_ref_swap]
constant ST.Prim.Ref.swap {σ : Type} {α : Type} (r : ST.Ref σ α) (a : α) :
ST σ α
source
@[extern lean_st_ref_take]
unsafe constant ST.Prim.Ref.take {σ : Type} {α : Type} (r : ST.Ref σ α) :
ST σ α
source
@[extern lean_st_ref_ptr_eq]
constant ST.Prim.Ref.ptrEq {σ : Type} {α : Type} (r1 : ST.Ref σ α) (r2 : ST.Ref σ α) :
ST σ Bool
source
@[inline]
unsafe def ST.Prim.Ref.modifyUnsafe {σ : Type} {α : Type} (r : ST.Ref σ α) (f : α → α) :
ST σ Unit
Equations
source
@[inline]
unsafe def ST.Prim.Ref.modifyGetUnsafe {σ : Type} {α : Type} {β : Type} (r : ST.Ref σ α) (f : α → β × α) :
ST σ β
Equations
source
@[implementedBy ST.Prim.Ref.modifyUnsafe]
noncomputable def ST.Prim.Ref.modify {σ : Type} {α : Type} (r : ST.Ref σ α) (f : α → α) :
ST σ Unit
Equations
source
@[implementedBy ST.Prim.Ref.modifyGetUnsafe]
noncomputable def ST.Prim.Ref.modifyGet {σ : Type} {α : Type} {β : Type} (r : ST.Ref σ α) (f : α → β × α) :
ST σ β
Equations
source
@[inline]
def ST.mkRef {σ : Type} {m : Type → Type} [inst : MonadLiftT (ST σ) m] {α : Type} (a : α) :
m (ST.Ref σ α)
Equations
source
@[inline]
def ST.Ref.get {σ : Type} {m : Type → Type} [inst : MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) :
m α
Equations
source
@[inline]
def ST.Ref.set {σ : Type} {m : Type → Type} [inst : MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) (a : α) :
m Unit
Equations
source
@[inline]
def ST.Ref.swap {σ : Type} {m : Type → Type} [inst : MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) (a : α) :
m α
Equations
source
@[inline]
unsafe def ST.Ref.take {σ : Type} {m : Type → Type} [inst : MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) :
m α
Equations
source
@[inline]
def ST.Ref.ptrEq {σ : Type} {m : Type → Type} [inst : MonadLiftT (ST σ) m] {α : Type} (r1 : ST.Ref σ α) (r2 : ST.Ref σ α) :
m Bool
Equations
source
@[inline]
def ST.Ref.modify {σ : Type} {m : Type → Type} [inst : MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) (f : α → α) :
m Unit
Equations
source
@[inline]
def ST.Ref.modifyGet {σ : Type} {m : Type → Type} [inst : MonadLiftT (ST σ) m] {α : Type} {β : Type} (r : ST.Ref σ α) (f : α → β × α) :
m β
Equations