[Agda] String -> Nat
Serge D. Mechveliani
mechvel at botik.ru
Mon Apr 15 14:13:01 CEST 2013
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,
> On 15.04.2013 10:23, Serge D. Mechveliani wrote:
> >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.
More information about the Agda