diff options
| author | Ana | 2020-12-01 08:52:12 +0000 |
|---|---|---|
| committer | Ana | 2021-02-26 13:32:41 +0000 |
| commit | 4302a75d82b9ac983cd89dd01c742c36777d921b (patch) | |
| tree | 8f6f437bb65bc3534e7f0f9851cdb05627ec885e /interp/notation.mli | |
| parent | 15074f171cdf250880bd0f7a2806356040c89f36 (diff) | |
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.
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index 97955bf92e..77f245ae77 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -137,11 +137,14 @@ type number_ty = hexadecimal : Names.inductive; number : Names.inductive } +type pos_neg_int63_ty = + { pos_neg_int63_ty : Names.inductive } + type target_kind = | Int of int_ty (* Coq.Init.Number.int + uint *) | UInt of int_ty (* Coq.Init.Number.uint *) | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) - | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *) + | Int63 of pos_neg_int63_ty (* Coq.Numbers.Cyclic.Int63.PrimInt63.pos_neg_int63 *) | Number of number_ty (* Coq.Init.Number.number + uint + int *) | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *) | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *) |