Idris2Doc : Data.Late

Data.Late

Definitions

dataLate : Type->Type
Totality: total
Visibility: public export
Constructors:
Now : a->Latea
Later : Inf (Latea) ->Latea

Hints:
ApplicativeLate
FunctorLate
MonadLate
never : Latea
  Never return

Totality: total
Visibility: public export
unfold : (seed->Eitherseedvalue) ->seed->Latevalue
  Run a small state machine until it reaches a final state and yields a value.

Totality: total
Visibility: public export
bind : Latea-> (a->Lateb) ->Lateb
  It's easier to define map and (<*>) in terms of bind so let's start
by defining it.

Totality: total
Visibility: public export
isNow : Latea->Maybea
  Check whether we already have a value.

Totality: total
Visibility: public export
wait : Latea->Latea
  Wait for one tick, hoping to get a value.

Totality: total
Visibility: public export
engine : Nat->Latea->Latea
  Wait for a set number of ticks.

Totality: total
Visibility: public export
petrol : Nat->Latea->Maybea
  Wait for a set number of ticks, hoping to get a value.

Totality: total
Visibility: public export
accelerate : Latea->Latea
  Accelerate makes things happen twice as fast.

Totality: total
Visibility: public export