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

Equations

• EST ε σ = EStateM ε σ

Instances For

• instInhabitedEST
• instMonadEST
• instMonadExceptOfEST
• instMonadLiftSTEST
• instSTWorldEST

@[inline, reducible]

abbrev ST (σ : Type) : Type → Type

Equations

• ST σ = EST Empty σ

Instances For

• IO.instMonadLiftSTRealWorldBaseIO
• Lean.MetavarContext.instMonadMCtxStateRefT'MetavarContextST
• Lean.instMonadMCtxStateRefT'MetavarContextST
• instMonadLiftSTEST
• instMonadST

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

Equations

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

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

Equations

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

instance instInhabitedEST {ε : Type} {σ : Type} {α : 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

• instSTWorld
• instSTWorldEST

instance instSTWorld {σ : Type} {m : Type → Type} {n : Type → Type} [MonadLift 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

• 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} {σ : Type} : MonadLift (ST σ) (EST ε σ)

Equations

• instMonadLiftSTEST = { monadLift := fun {α} x s => match x s with | EStateM.Result.ok a s => EStateM.Result.ok a s | EStateM.Result.error ex a => nomatch ex }

opaque ST.RefPointed : NonemptyType

References

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

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

Instances For

• ST.instNonemptyRef

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

Equations

• @ST.instNonemptyRef = @ST.instNonemptyRef.proof_1

@[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 : α) : ST σ Unit

@[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 σ α) : ST σ Bool

@[inline]

unsafe def ST.Prim.Ref.modifyUnsafe {σ : Type} {α : Type} (r : ST.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} {α : Type} {β : Type} (r : ST.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} {α : Type} (r : ST.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} {α : Type} {β : Type} (r : ST.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 (ST.Ref σ α)

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

• ST.Ref.swap r 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 α

Equations

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

@[inline]

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

Equations

• ST.Ref.ptrEq r1 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

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

@[inline]

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

Equations

• ST.Ref.modifyGet r 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

• ST.Ref.toMonadStateOf r = { get := ST.Ref.get r, set := ST.Ref.set r, modifyGet := fun {α} => ST.Ref.modifyGet r }