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

Equations

• EST ε σ = EStateM ε σ

Instances For

• instInhabitedEST
• instMonadEST
• instMonadExceptOfEST
• instMonadLiftSTEST
• instSTWorldEST

@[reducible, inline]

abbrev ST (σ : Type) : Type → Type

Equations

• ST σ = EST Empty σ

Instances For

• IO.instMonadLiftSTRealWorldBaseIO
• instMonadLiftSTEST
• instMonadST

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

Instances

• instSTWorldEST
• instSTWorldOfMonadLift

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

Equations

• instSTWorldOfMonadLift = { }

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

Equations

• instSTWorldEST = { }

@[noinline]

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

Equations

• runEST x = match x Unit () with | EStateM.Result.ok a a_1 => Except.ok a | EStateM.Result.error ex a => Except.error ex

@[noinline]

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

Equations

• runST x = match x Unit () with | EStateM.Result.ok a a_1 => a | EStateM.Result.error ex a => nomatch ex

@[always_inline]

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

Equations

• One or more equations did not get rendered due to their size.

opaque ST.RefPointed : NonemptyType

References

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

• ref : RefPointed.type
• h : Nonempty α

Instances For

• ST.instNonemptyRef

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

@[extern lean_st_mk_ref]

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

@[extern lean_st_ref_get]

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

@[extern lean_st_ref_set]

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

@[extern lean_st_ref_swap]

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

@[extern lean_st_ref_take]

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

@[extern lean_st_ref_ptr_eq]

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

@[inline]

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

Equations

• ST.Prim.Ref.modifyUnsafe r f = do let v ← ST.Prim.Ref.take r ST.Prim.Ref.set r (f v)

@[inline]

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

Equations

• ST.Prim.Ref.modifyGetUnsafe r f = do let v ← ST.Prim.Ref.take r match f v with | (b, a) => do ST.Prim.Ref.set r a pure b

@[implemented_by ST.Prim.Ref.modifyUnsafe]

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

Equations

• ST.Prim.Ref.modify r f = do let v ← ST.Prim.Ref.get r ST.Prim.Ref.set r (f v)

@[implemented_by ST.Prim.Ref.modifyGetUnsafe]

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

Equations

• ST.Prim.Ref.modifyGet r f = do let v ← ST.Prim.Ref.get r match f v with | (b, a) => do ST.Prim.Ref.set r a pure b

@[inline]

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

Equations

• ST.mkRef a = liftM (ST.Prim.mkRef a)

@[inline]

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

Equations

• r.get = liftM (ST.Prim.Ref.get r)

@[inline]

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

Equations

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

@[inline]

def ST.Ref.swap {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r : 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 : Ref σ α) : m α

Equations

• r.take = liftM (ST.Prim.Ref.take r)

@[inline]

def ST.Ref.ptrEq {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type} (r1 r2 : 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 : 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 : 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 : Ref σ α) : MonadStateOf α m

Equations

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