Skip to content

Instantly share code, notes, and snippets.

@turion

turion/Live.idr

Last active July 2, 2017 18:20
Show Gist options
  • Save turion/2203bf029528a07e4b00c8a1d34959a1 to your computer and use it in GitHub Desktop.
Save turion/2203bf029528a07e4b00c8a1d34959a1 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment