[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