coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How does Int31 "underlying mechanism for hardware-efficient computations" work?

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] How does Int31 "underlying mechanism for hardware-efficient computations" work?
Date: Tue, 28 Jun 2016 10:42:13 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga09.intel.com
Ironport-phdr: 9a23:QSs5KBXKwA1ltXUEQgNixJWLvLLV8LGtZVwlr6E/grcLSJyIuqrYZhKCt8tkgFKBZ4jH8fUM07OQ6PG4HzVbqsze+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLshrj0osaYOVoArQH+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBO/xeL19RrhFBhwnNXo07Yvlr1OLGQCI/z4XVngcuhtOGQnMqh/gCMTfqCz/46BG3ySVIdfxVfR8fDWp765mTFWg3CIGPD4w/WWRkct9g75BpwqJphpjzoqSa4aQYqktNpjBdM8XEDISFv1aUDZMV9ux

Dear Coq Users,

the In31 library

https://coq.inria.fr/library/Coq.Numbers.Cyclic.Int31.Int31.html

states that the Int31 type comes with an “underlying mechanism for hardware-efficient computations”. I wonder what this means and how it works. The addition in Int31 seems to be implemented by conversion to Z, addition in Z and conversion back.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] How does Int31 "underlying mechanism for hardware-efficient computations" work?, Soegtrop, Michael, 06/28/2016
- RE: [Coq-Club] How does Int31 "underlying mechanism for hardware-efficient computations" work?, Soegtrop, Michael, 06/28/2016
  - Re: [Coq-Club] How does Int31 "underlying mechanism for hardware-efficient computations" work?, Arnaud Spiwack, 06/28/2016
    - RE: [Coq-Club] How does Int31 "underlying mechanism for hardware-efficient computations" work?, Soegtrop, Michael, 06/29/2016
      - Re: [Coq-Club] How does Int31 "underlying mechanism for hardware-efficient computations" work?, Laurent Thery, 06/29/2016
        
        Re: [Coq-Club] How does Int31 "underlying mechanism for hardware-efficient computations" work?, Arnaud Spiwack, 06/29/2016
        
        RE: [Coq-Club] How does Int31 "underlying mechanism for hardware-efficient computations" work?, Soegtrop, Michael, 06/30/2016