@[reducible, inline]

abbrev Std.AtomicT (σ : Type) (m : Type → Type) (α : Type) : Type

AtomicT α m is the monad that can be atomically executed inside mutual exclusion primitives like Mutex α with outside monad m. The action has access to the state α of the mutex (via get and set).

Equations

• Std.AtomicT = StateRefT' IO.RealWorld