[Agda] file for readFiniteFile

[Sergei Meshveliani]

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

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...>

I need to parse a number from the input string, and apply
`initStr' (drop last character) to the string before parsing.
(I doubt of whether this is a nice solution). 

My question was: how to obtain the input string without any parasitic
last character and without any additional processing of the input
string. 

Sorry for somewhat a stupid question.

------
Sergei