coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] large numbers in Gallina

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] large numbers in Gallina
Date: Sun, 20 Dec 2020 13:10:56 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f171.google.com
Ironport-phdr: 9a23:CD74QRVbhque3jVGtcSZbRsdM9DV8LGtZVwlr6E/grcLSJyIuqrYbRWGt8tkgFKBZ4jH8fUM07OQ7/m/HzZYud3Y6StKWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oIxi6sAfcutMIjYd+Nqo9xQbFrmZGdu9L2W5mOFWfkgrm6Myt5pBj6SNQu/wg985ET6r3erkzQKJbAjo7LW07/dXnuhbfQwSB4HscSXgWnQFTAwfZ9hH6X4z+vTX8u+FgxSSVJ8z2TbQzWTS/86dmTQLjhSkbOzIl9mzcl8p9h79Zrh28vRxy24DaboGLOvRjfa3TetwVSnZOUMtKSyxMAJmxY5cVAuYdI+pVqZT2qVsUrRu5AAmhHO3jyj1Phn/w3K060PouEQXY0wM+BN8Ov3HUo8/0NKcWS+y60K7IzTDNY/hL3jr96o/IchYgofGPQ71wddTexlc0GgPKi1Wfs43lPzeP2usRtGib6vNtWOSygGEotw9/uCKgxtswiobXnIIVzEjJ+Th5zYg1KtC1VlJ3bMKkHZZSuSyXK4R7Tt8iTm11tig21rkLtJ+7ciUJ1pkr2wLSZuGZf4WK/h/uSeicLDd2in9jZbmxhA6y/FC+xuHgUsS4ylVHoypfntXRt30Bywbf5tWFR/dg5kutxzeC2xzO5uxBPEw5kbbUJpsuz7MxipYfrUHOEjLqlErsiaKZbUYp9fam6+nifLnmqJGcN4FxhwHwLKsulMOyDOE2MgUBUGWb9+Kx36D580LjWrVFlPg2n7HZsJ/EIcQboba0AwpP3YYi7xazFi6m0MgFkXUeIlJJZRCKg5XzN1HBJ/D4Cvi/g1Cynztx2//GObjhDo3MLnjFjrjhYa5w51BAxAc319xS5JJZBqscLP/yRkP9rsHUAx0kPwCsxuboEtR91ocQWWKVBa+ZNbvfsV2P5uIpIumMZ5EauDLjJPc7/PPugno5lkUcfamtx5cYdHe4HvF+L0WDfXXsmssBEXsNvgcmUOPqj0SCXSdPaHa2QqIz/So2CJmmDIfGXoCimqaN3Ca9Hp1MZ2BJEEqAEXnyd9bMZ/BZYyWLZ8RljzZMAbOmUsoq0QyknA780btuaOTOrH42r5XmgZJ34OvSlhw2+DFcAMGU0mXLRGZx1CtcRTgw3aNypUFw4liG2Kl8xfdfEIoAtLtyTg4mOMuEnKRBANfoV1eZJ4bbeBOdWtyjRAoJYJc0yt4KbVx6Hoz73B/G1iuuRbQSku7SXcFmwufnx3H0Yv1F5TPG2a0m1Qd0R8JOMSi/mvc6+VGMXsjGlEKWk6vsfqMZjnaUqDWziFGWtUQdazZeFL3fVClGNETTpNX9oEjFSu32BA==

What is the best performing way to use large numbers in Gallina? I am
getting the following warning, which seems to imply I could have done
something better with this definition:

Definition fuel : nat := 10000.

Warning: To avoid stack overflow, large numbers in nat are interpreted
as applications of Nat.of_num_uint. [abstract-large-number,numbers]
fuel is defined

[Coq-Club] large numbers in Gallina, jonikelee AT gmail.com, 12/20/2020
- Re: [Coq-Club] large numbers in Gallina, Guillaume Melquiond, 12/21/2020
  - Re: [Coq-Club] large numbers in Gallina, Xavier Leroy, 12/21/2020
    - Re: [Coq-Club] large numbers in Gallina, Guillaume Melquiond, 12/21/2020