def EST (ε σ : Type) : Type → Type

Equations

• EST ε σ = EStateM ε σ

@[reducible, inline]

abbrev ST (σ : Type) : Type → Type

instance instMonadEST (ε σ : Type) : Monad (EST ε σ)

Equations

• instMonadEST ε σ = inferInstanceAs (Monad (EStateM ε σ))

instance instMonadExceptOfEST (ε σ : Type) : MonadExceptOf ε (EST ε σ)

Equations

• instMonadExceptOfEST ε σ = inferInstanceAs (MonadExceptOf ε (EStateM ε σ))

instance instInhabitedEST {ε σ α : Type} [Inhabited ε] : Inhabited (EST ε σ α)

Equations

• instInhabitedEST = inferInstanceAs (Inhabited (EStateM ε σ α))

instance instMonadST (σ : Type) : Monad (ST σ)

Equations

• instMonadST σ = inferInstanceAs (Monad (EST Empty σ))

class STWorld (σ : outParam Type) (m : Type → Type) : Type

instance instSTWorldOfMonadLift {σ : Type} {m n : Type → Type} [MonadLift m n] [STWorld σ m] : STWorld σ n

instance instSTWorldEST {ε σ : Type} : STWorld σ (EST ε σ)

Equations

• instSTWorldEST = { }

@[noinline]

def runEST {ε α : Type} (x : (σ : Type) → EST ε σ α) : Except ε α

@[noinline]

def runST {α : Type} (x : (σ : Type) → ST σ α) : α

@[always_inline]

instance instMonadLiftSTEST {ε σ : Type} : MonadLift (ST σ) (EST ε σ)

opaque ST.RefPointed : NonemptyType

References

structure ST.Ref (σ α : Type) : Type

• ref : ST.RefPointed.type
• h : Nonempty α

theorem ST.instNonemptyRef {σ α : Type} [s : Nonempty α] : Nonempty (ST.Ref σ α)

@[extern lean_st_mk_ref]

opaque ST.Prim.mkRef {σ α : Type} (a : α) : ST σ (ST.Ref σ α)

@[extern lean_st_ref_get]

opaque ST.Prim.Ref.get {σ α : Type} (r : ST.Ref σ α) : ST σ α

@[extern lean_st_ref_set]

opaque ST.Prim.Ref.set {σ α : Type} (r : ST.Ref σ α) (a : α) : ST σ Unit

@[extern lean_st_ref_swap]

opaque ST.Prim.Ref.swap {σ α : Type} (r : ST.Ref σ α) (a : α) : ST σ α

@[extern lean_st_ref_take]

unsafe opaque ST.Prim.Ref.take {σ α : Type} (r : ST.Ref σ α) : ST σ α

@[extern lean_st_ref_ptr_eq]

opaque ST.Prim.Ref.ptrEq {σ α : Type} (r1 r2 : ST.Ref σ α) : ST σ Bool

@[inline]

unsafe def ST.Prim.Ref.modifyUnsafe {σ α : Type} (r : ST.Ref σ α) (f : α → α) : ST σ Unit

@[inline]

unsafe def ST.Prim.Ref.modifyGetUnsafe {σ α β : Type} (r : ST.Ref σ α) (f : α → β × α) : ST σ β

@[implemented_by ST.Prim.Ref.modifyUnsafe]

def ST.Prim.Ref.modify {σ α : Type} (r : ST.Ref σ α) (f : α → α) : ST σ Unit

@[implemented_by ST.Prim.Ref.modifyGetUnsafe]

def ST.Prim.Ref.modifyGet {σ α β : Type} (r : ST.Ref σ α) (f : α → β × α) : ST σ β

@[inline]

def ST.mkRef {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (a : α) : m (ST.Ref σ α)

@[inline]

def ST.Ref.get {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) : m α

@[inline]

def ST.Ref.set {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) (a : α) : m Unit

@[inline]

def ST.Ref.swap {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) (a : α) : m α

Equations

• r.swap a = liftM (ST.Prim.Ref.swap r a)

@[inline]

unsafe def ST.Ref.take {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) : m α

@[inline]

def ST.Ref.ptrEq {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r1 r2 : ST.Ref σ α) : m Bool

Equations

• r1.ptrEq r2 = liftM (ST.Prim.Ref.ptrEq r1 r2)

@[inline]

def ST.Ref.modify {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) (f : α → α) : m Unit

Equations

• r.modify f = liftM (ST.Prim.Ref.modify r f)

@[inline]

def ST.Ref.modifyGet {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α β : Type} (r : ST.Ref σ α) (f : α → β × α) : m β

Equations

• r.modifyGet f = liftM (ST.Prim.Ref.modifyGet r f)

def ST.Ref.toMonadStateOf {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : ST.Ref σ α) : MonadStateOf α m

Equations

• r.toMonadStateOf = { get := r.get, set := r.set, modifyGet := fun {α_1 : Type} => r.modifyGet }