[Agda] file for readFiniteFile

Nils Anders Danielsson nad at cse.gu.se
Thu Sep 22 15:10:04 CEST 2016


On 2016-09-22 14:48, Sergei Meshveliani wrote:
> If you set
>             12
>
> into  data.txt,  the result string will have length 3.
> I guess that the last symbol is Newline, because this is visible on the
> screen output when running `main':
>
>    ...> ./TT
>    12
>    ...>
>
> instead of
>
>    ...> ./TT
>    12...>

If I insert "12\n" into data.txt, then the program prints a newline
character, and if I insert "12", then it doesn't.

-- 
/NAD


More information about the Agda mailing list