[Agda] file for readFiniteFile

[Sergei Meshveliani]

On Thu, 2016-09-22 at 15:10 +0200, Nils Anders Danielsson wrote:
> 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.
> 

1) "12" contains the two additional characters (`"').
   Do you mean  12  
   ? 

2) I set characters into  data.txt  by using the  emacs  editor.
Probably this  emacs  appends an additional character (Newline) itself.

3) Now, I tried the  joe  editor, and it does not append Newline !

Probably, a reliable program (written in Agda)  for this example  needs
 
  to input  str  from file and then to filter in  str  the characters 
  that are decimal digits.

This way it would not depend on the editor used.

Regards,

------
Sergei