fact: Definition sleep_plenty `{Monad m, MonadFile m, MonadSleep m} (d : i63) : m unit := write std_out "Hello...";; let y : tuple4 i63 i63 i63 i63 := mktuple4 1 2 3 4 in match y with | mktuple4 a b c d => let x := (a * b + c - d) / d in sleep x;; write std_out " sleepy world!\n" end.
imports: Coq(Extraction) SimpleIO(SimpleIO) ExtLib(Monad) CoqFFI(Extraction) Examples(File Sleep Records) CoqFFI(String)