The Coq mailing list

[David Pereira <dpereira AT liacc.up.pt>]

Hi,


> 
> I was unable to find a work in the users' contributions that uses it, but I 
> imagine there exists with such a need... 
> 
> could you please point me to a development that uses lists to represent 
> (large) natural numbers?

Isn't the type [N] enough for you? It is available in the NArith module of 
the standard library. The type [N] is a binary encoding of natural numbers 
and is efficient when compared to the Peano representation.


Cheers,
        David.


> 
> -- 
> Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 
> dollars last year.
> Marge: Bart! Don't make fun of grad students, they just made a terrible 
> life choice.