From 4302a75d82b9ac983cd89dd01c742c36777d921b Mon Sep 17 00:00:00 2001 From: Ana Date: Tue, 1 Dec 2020 08:52:12 +0000 Subject: Signed primitive integers Signed primitive integers defined on top of the existing unsigned ones with two's complement. The module Sint63 includes the theory of signed primitive integers that differs from the unsigned case. Additions to the kernel: les (signed <=), lts (signed <), compares (signed compare), divs (signed division), rems (signed remainder), asr (arithmetic shift right) (The s suffix is not used when importing the Sint63 module.) The printing and parsing of primitive ints was updated and the int63_syntax_plugin was removed (we use Number Notation instead). A primitive int is parsed / printed as unsigned or signed depending on the scope. In the default (Set Printing All) case, it is printed in hexadecimal. --- doc/stdlib/index-list.html.template | 1 + 1 file changed, 1 insertion(+) (limited to 'doc/stdlib') diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index cbe526be68..27eb64a83b 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -286,6 +286,7 @@ through the Require Import command.

theories/Numbers/Cyclic/Int63/Cyclic63.v theories/Numbers/Cyclic/Int63/PrimInt63.v theories/Numbers/Cyclic/Int63/Int63.v + theories/Numbers/Cyclic/Int63/Sint63.v theories/Numbers/Cyclic/Int63/Ring63.v theories/Numbers/Cyclic/ZModulo/ZModulo.v -- cgit v1.2.3