Idris2Doc : IO.Async.BQueue

IO.Async.BQueue

(source)

Definitions

recordBQueue : Type->Type
  A concurrent, bounded queue holding values of type `a`.

This is an important primitive for implementing producer/consumer
services.

Totality: total
Visibility: export
Constructor: 
BQ : IORef (STa) ->BQueuea

Projection: 
.ref : BQueuea->IORef (STa)
bqueue : Lift1Worldf=>Nat->f (BQueuea)
  Creates a new bounded queue of the given capacity.

Totality: total
Visibility: export
bqueueOf : Lift1Worldf=> (0a : Type) ->Nat->f (BQueuea)
  Utility alias for `bqueue` taking the type of stored values
as an explicit argument.

Totality: total
Visibility: export
enqueue : BQueuea->a->Asyncees ()
  Appends a value to a bounded queue potentially blocking the
calling fiber until there is some capacity.

Totality: total
Visibility: export
dequeue : BQueuea->Asynceesa
  Extracts the next value from a bounded queue potentially blocking
the calling fiber until such a value is available.

Totality: total
Visibility: export