[Agda] Re: String -> Nat

[Benjamin Barenblat]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

>> On 15.04.2013 10:23, Serge D. Mechveliani wrote:
>>>what Standard library has for reading (parsing)  Nat  from String
>>>(or List Char) ?

> On Mon, Apr 15, 2013 at 01:15:00PM +0200, Andreas Abel wrote:
>> There is one in the Agda Prelude,

On Monday, April 15, 2013, at  8:13 am EDT, Serge D. Mechveliani wrote:
> 3) Prelude  has such, but Prelude is not in standard
>    (besides, I could not compile Prelude in previous Agda version).

As a bit of an exercise, I ported 'stringToℕ' from the Agda Prelude to
the standard library; see <http://hpaste.org/85901>.  It compiles under
Agda 2.3.0 / stdlib 0.6.

I’m not sure why we don’t have this in the standard library – perhaps a
more experienced Agda programmer can shed some light on the topic.  Is
it merely to keep the standard library small?  Or is this type of
function considered out of place?

Benjamin
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.19 (GNU/Linux)

iQEcBAEBCgAGBQJRbUFiAAoJEJ5zAUnrkcU7h+8H/0GUIqbWgVYH2HCUuArNTABx
L1IQTzCQziYC1cj9xYOHsCTv7iz7c3pubYX+vR5JAbqaEtEuqEJgvnj4xEOd654l
PgtLr/zMyN/h18RR/Mcv2xIYG98CMuya6qJ893+y+wHVWvH9sTJzCNeEZRdqrQhq
sRAjsnhgtPnPGmyh/pR56+bWJFBKwyo57JCz+N3Oo0O/aP5NKqpa6mr1xGIG6EEc
v+NQWvSKlTIzmNwW9oR7EEZqrcK50cJVe7nvV8D+ZciIKkNNMlKDfodFhalJqg4p
4/NG+GwvvDcWQ6c12IJl0vdIUw42asYzNS7eewScHMOVjvvmyXoEf6Kzn90LQP4=
=bpO6
-----END PGP SIGNATURE-----