fact: Definition cat `{Monad m, MonadFile m} : m unit := let* fd := openfile "README.md" in let* content := read_all fd in write std_out content;; closefile fd.
imports: Coq(Extraction) SimpleIO(SimpleIO) ExtLib(Monad) CoqFFI(Extraction) Examples(File Sleep Records) CoqFFI(String)