Idris2Doc : Data.Late

Data.Late

dataLate : Type -> Type
Totality: total
Constructors:
Now : a -> Latea
Later : Inf (Latea) -> Latea
accelerate : Latea -> Latea
  Accelerate makes things happen twice as fast.

Totality: total
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
engine : Nat -> Latea -> Latea
  Wait for a set number of ticks.

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

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

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

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

Totality: total