Evince.Synchronized

Definitions

record Lock : (Type -> Type) -> Type

  A lock: a function that runs an action while holding mutual exclusion, for
  any result type. `Synchronized.newLock` allocates one.

Totality: total
Visibility: public export
Constructor: 

MkLock : (m a -> m a) -> Lock m

Projection: 

.withLock : Lock m -> m a -> m a

.withLock : Lock m -> m a -> m a

Totality: total
Visibility: public export

withLock : Lock m -> m a -> m a

Totality: total
Visibility: public export

interface Synchronized : (Type -> Type) -> Type

  A monad whose actions can run under mutual exclusion. Sequential `IO` runs
  can't race, so its lock is a no-op; a concurrent driver provides a real lock.

Parameters: m
Methods:

newLock : IO (Lock m)

Implementation: 

Synchronized IO

newLock : Synchronized m => IO (Lock m)

Totality: total
Visibility: public export