<div dir="ltr"><div dir="ltr"><div dir="ltr"><a href="https://youtu.be/QuTVX7_BjpE">https://youtu.be/QuTVX7_BjpE</a></div><div dir="ltr"><br></div><div dir="ltr">```<br></div><div dir="ltr">module UniK where<br><br>open import Prelude.IO<br>open import Prelude.Monad<br>open import Prelude.Unit<br>open import Prelude.Nat<br>open import Prelude.String<br><br><br>postulate<br>  info : String -> IO Unit<br><br>{-# FOREIGN OCaml<br>let info s world = Logs_lwt.info (fun f -> f (Scanf.format_from_string s "lofs"))<br>#-}<br><br>{-# COMPILE OCaml info = info #-}<br><br>loop : IO Unit → Nat → IO Unit<br>loop sleep zero = return unit<br>loop sleep (suc n) = do<br>  info "Hello from Agda."<br>  sleep<br>  loop sleep n<br><br><br>start : IO Unit → IO Unit<br>start sleep = loop sleep 4<br><br><br>{-# COMPILE OCaml start as val start : (unit -> unit Lwt.t) -> unit -> unit Lwt.t #-}<br><br>```<br></div></div></div>