Documentation

Init.System.ST

source
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 {σ : Type} {m : Type → Type} {n : Type → Type} [inst : MonadLift m n] [inst : STWorld σ m] :
    STWorld σ n
    Equations
    • instSTWorld = { }
    source
    instance instSTWorldEST {ε : Type} {σ : 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
    opaque ST.RefPointed:
    NonemptyType
    source
    structure ST.Ref (σ : Type) (α : Type) :
    Type
    source
    instance ST.instNonemptyRef {σ : Type} {α : Type} [s : Nonempty α] :
    Nonempty (ST.Ref σ α)
    Equations
    source
    @[extern lean_st_mk_ref]
    opaque ST.Prim.mkRef {σ : Type} {α : Type} (a : α) :
    ST σ (ST.Ref σ α)
    source
    @[extern lean_st_ref_get]
    opaque ST.Prim.Ref.get {σ : Type} {α : Type} (r : ST.Ref σ α) :
    ST σ α
    source
    @[extern lean_st_ref_set]
    opaque ST.Prim.Ref.set {σ : Type} {α : Type} (r : ST.Ref σ α) (a : α) :
    ST σ Unit
    source
    @[extern lean_st_ref_swap]
    opaque ST.Prim.Ref.swap {σ : Type} {α : Type} (r : ST.Ref σ α) (a : α) :
    ST σ α
    source
    @[extern lean_st_ref_take]
    unsafe opaque ST.Prim.Ref.take {σ : Type} {α : Type} (r : ST.Ref σ α) :
    ST σ α
    source
    @[extern lean_st_ref_ptr_eq]
    opaque 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]
    def ST.Prim.Ref.modify {σ : Type} {α : Type} (r : ST.Ref σ α) (f : α → α) :
    ST σ Unit
    Equations
    source
    @[implementedBy ST.Prim.Ref.modifyGetUnsafe]
    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