[Agda] Re: String -> Nat
benjamin at barenblat.name
Tue Apr 16 14:17:33 CEST 2013
-----BEGIN PGP SIGNED MESSAGE-----
>> 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?
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.19 (GNU/Linux)
-----END PGP SIGNATURE-----
More information about the Agda