Live.idr

record Live a where
  constructor LiveC
  state : Type
  step : state -> (a, state)

bind : Live (Live a) -> Live a
bind {a} (LiveC state1 step1) = LiveC newstate f where
  f (sta1 ** st2) = (?aVal, (?st1' ** ?st2'))
  newstate : Type
  newstate = (st1 : state1 ** state (fst (step1 st1)))