opaque Void.nonemptyType (σ : Type) : NonemptyType

def Void (σ : Type) : Type

instance Void.instNonempty {σ : Type} : Nonempty (Void σ)

@[never_extract, extern lean_void_mk]

opaque Void.mk {σ : Type} (x : σ) : Void σ

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

• val : α
• state : Void σ

def ST (σ α : Type) : Type

A restricted version of IO in which mutable state is the only side effect.

It is possible to run ST computations in a non-monadic context using runST.

@[inline]

def ST.pure {α σ : Type} (x : α) : ST σ α

@[inline]

def ST.bind {σ α β : Type} (x : ST σ α) (f : α → ST σ β) : ST σ β

@[implicit_reducible]

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

@[implicit_reducible, always_inline]

instance instMonadFinallyST {σ : Type} : MonadFinally (ST σ)

@[implicit_reducible]

instance instInhabitedST {σ α : Type} [Inhabited α] : Inhabited (ST σ α)

@[implicit_reducible]

instance instMonadAttachST {σ : Type} : MonadAttach (ST σ)

inductive EST.Out (ε σ α : Type) : Type

• ok {ε σ α : Type} : α → Void σ → Out ε σ α
• error {ε σ α : Type} : ε → Void σ → Out ε σ α

def EST (ε σ α : Type) : Type

A restricted version of IO in which mutable state and exceptions are the only side effects.

It is possible to run EST computations in a non-monadic context using runEST.

@[inline]

def EST.pure {α ε σ : Type} (a : α) : EST ε σ α

@[inline]

def EST.bind {ε σ α β : Type} (x : EST ε σ α) (f : α → EST ε σ β) : EST ε σ β

@[inline]

def EST.throw {ε σ α : Type} (e : ε) : EST ε σ α

@[inline]

def EST.tryCatch {ε σ α : Type} (x : EST ε σ α) (handle : ε → EST ε σ α) : EST ε σ α

@[implicit_reducible]

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

@[implicit_reducible, always_inline]

instance instMonadFinallyEST {ε σ : Type} : MonadFinally (EST ε σ)

@[implicit_reducible]

instance instMonadAttachEST {ε σ : Type} : MonadAttach (EST ε σ)

@[implicit_reducible]

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

@[implicit_reducible]

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

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

An auxiliary class used to infer the “state” of EST and ST monads.

@[implicit_reducible]

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

@[implicit_reducible]

instance instSTWorldST {σ : Type} : STWorld σ (ST σ)

@[implicit_reducible]

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

@[noinline]

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

Runs an EST computation, in which mutable state and exceptions are the only side effects.

@[noinline]

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

Runs an ST computation, in which mutable state via ST.Ref is the only side effect.

@[implicit_reducible, always_inline]

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

opaque ST.RefPointed : NonemptyType

References

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

Mutable reference cells that contain values of type α. These cells can read from and mutated in the ST σ monad.

• ref : RefPointed.type
• h : Nonempty α

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

@[inline]

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

@[implemented_by ST.Prim.Ref.modifyUnsafe]

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

@[implemented_by ST.Prim.Ref.modifyGetUnsafe]

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

@[inline]

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

Creates a new mutable reference that contains the provided value a.

@[inline]

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

Reads the value of a mutable reference.

@[inline]

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

Replaces the value of a mutable reference.

@[inline]

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

Atomically swaps the value of a mutable reference cell with another value. The reference cell's original value is returned.

@[inline]

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

Reads the value of a mutable reference cell, removing it.

This causes subsequent attempts to read from or take the reference cell to block until a new value is written using ST.Ref.set.

@[inline]

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

Checks whether two reference cells are in fact aliases for the same cell.

Even if they contain the same value, two references allocated by different executions of IO.mkRef or ST.mkRef are distinct. Modifying one has no effect on the other. Likewise, a single reference cell may be aliased, and modifications to one alias also modify the other.

@[inline]

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

Atomically modifies a mutable reference cell by replacing its contents with the result of a function call.

@[inline]

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

Atomically modifies a mutable reference cell by replacing its contents with the result of a function call that simultaneously computes a value to return.

@[implicit_reducible]

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

Creates a MonadStateOf instance from a reference cell.

This allows programs written against the state monad API to be executed using a mutable reference cell to track the state.