@[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).