The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

I found it. The “Register” declarations get stripped from the generated documentation:

 

Register digits as int31 bits in "coq_int31" by True.

Register int31 as int31 type in "coq_int31" by True.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Soegtrop, Michael
Sent: Tuesday, June 28, 2016 12:42 PM
To: coq-club AT inria.fr
Subject: [Coq-Club] How does Int31 "underlying mechanism for hardware-efficient computations" work?

 

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

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