Data.Late

Definitions

data Late : Type -> Type

Totality: total
Visibility: public export
Constructors:

Now : a -> Late a

Later : Inf (Late a) -> Late a

Hints:

Applicative Late

Functor Late

Monad Late

never : Late a

  Never return

Totality: total
Visibility: public export

unfold : (seed -> Either seed value) -> seed -> Late value

  Run a small state machine until it reaches a final state and yields a value.

Totality: total
Visibility: public export

bind : Late a -> (a -> Late b) -> Late b

  It's easier to define map and (<*>) in terms of bind so let's start
  by defining it.

Totality: total
Visibility: public export

isNow : Late a -> Maybe a

  Check whether we already have a value.

Totality: total
Visibility: public export

wait : Late a -> Late a

  Wait for one tick, hoping to get a value.

Totality: total
Visibility: public export

engine : Nat -> Late a -> Late a

  Wait for a set number of ticks.

Totality: total
Visibility: public export

petrol : Nat -> Late a -> Maybe a

  Wait for a set number of ticks, hoping to get a value.

Totality: total
Visibility: public export

accelerate : Late a -> Late a

  Accelerate makes things happen twice as fast.

Totality: total
Visibility: public export