ex_5_3_5.idr

import Data.Vect

readToBlank : IO (List String)
readToBlank = do x <- getLine
                 if (x == "")
                    then pure []
                    else do xs <- readToBlank
                            pure (x :: xs)

readAndSave : IO ()
readAndSave = do xs <- readToBlank
                 filename <- getLine
                 Right h <- writeFile filename (unlines xs)
                   | Left err => putStrLn (show err)
                 pure ()
                                                   
readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile filename = do
  Right h <- openFile filename Read
  ?readVectFile_rhs