[Agda] file for readFiniteFile

Nils Anders Danielsson nad at cse.gu.se
Thu Sep 22 13:30:39 CEST 2016


On 2016-09-21 21:20, Sergei Meshveliani wrote:
> I put  12
>
> in the file  data.txt  and apply  (readFiniteFile "data.txt").
>
> And it returns  "120"  instead of expected  "12".

I'm not quite sure what you mean. The following code seems to work for
me:

   open import Data.String
   open import Function
   open import IO.Primitive

   main = readFiniteFile "data.txt" >>= putStr ∘ toCostring

If something is broken, please report this on the bug tracker, and
please provide a self-contained example.

-- 
/NAD


More information about the Agda mailing list