[Agda] String -> Nat

[Serge D. Mechveliani]

This looks a bit strange:
1) the checker does convert things like  12 : Nat  to  Nat,
2) Standard library has not a conversion of this type,
3) Prelude  has such, but Prelude is not in standard
   (besides, I could not compile Prelude in previous Agda version).



On Mon, Apr 15, 2013 at 01:15:00PM +0200, Andreas Abel wrote:
> There is one in the Agda Prelude,
> 
> https://github.com/fkettelhoit/agda-prelude/blob/master/Prelude.agda
> 
> On 15.04.2013 10:23, Serge D. Mechveliani wrote:
> >Please,
> >what Standard library has for reading (parsing)  Nat  from String
> >(or List Char) ?
> >For example,  "10" -> suc suc suc suc suc suc suc suc suc suc zero.
> >
> >I need to input Nat from a file, and use  readFile.
> >This produces  str : String  (may be Costring),
> >then,  str  needs to convert to Nat.
> >
> >Thanks,
> >
> >------
> >Sergei