The Coq mailing list

[Wojciech Meyer <wojciech.meyer AT gmail.com>]

Hi Nuno,

Nuno Gaspar 
<nmpgaspar AT gmail.com>
 writes:

> 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?

nat is meant to be designed for indexing other data types, using
dependent typing, like vectors or indexed lists and I don't think it can
be used efficiently in any other ways.

-Wojciech