[Agda] readFile and output

[Serge D. Mechveliani]

On Tue, Oct 02, 2012 at 02:07:07PM +0400, Serge D. Mechveliani wrote:
> People,
> I have a beginner question on  IO  in the  Standard Libarary lib-0.6
> (for Agda-2.3.0.1, MAlonzo).
> 
> The below small program intends to
> (1) read a string  str  (like "1011")  from the file "inp.txt",
> (2) convert  str  to  b : Bin,
> (3) show b  to  bStr : String  and print  bStr  to the screen.
> 
> I know how to arrange (2) and (3).
> But I need to find how to arrange the following operations related to 
> (1).
> [..]

Sorry for disturbance.  I have managed with using  _>>=_.

The remain the to minor questions, not so important:

1. Having a string like  "103" : String,  
   what is the simplest way to convert it to  Nat  (unary natural) ?
2. I convert  Colist -> List  by my home-made  takeFromColist.
   And  Colist.take  reports of error with  BoundedVec Char 2
   -- as I write in another letter.
   It is better to use a library function, though.  

Concerning a large list evaluation at the compilation time, I hope,
reading the counter from a file will helpя. I'll try this.

Thanks,

------
Sergei