Write a File in Idris

Although Idris' documentation seems better than 99% of opensource projects out there, I couldn't easily find the steps necessary to write a file. After recalling that Brian McKenna wrote his blog in Idris, I figured he would have a nice example of how to write a file and I was right! This post is heavily ripped from his work. The actual code (taken from the Main file of Brain's code generator) looks like

writeFile : String -> String -> IO ()
writeFile f s = do
  f <- openFile f Write
  fwrite f s
  closeFile f

Pretty straight forward. It takes a file name and the content to write, opens a handle, writes the contents to that file then closes it. Now, I had found and written code like this in Idris' docs, but couldn't get it to compile. The trick was to tell Idris to compile and include the effects package, like so

idris -p effects Main.idr -o my_program

Thanks Brian!