Idris2Doc : Data.Late

Data.Late

Late : 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