The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Thanks for the pointer, Ana!

On Tue, Dec 7, 2021 at 11:32 PM Ana Borges <ana.agvb AT gmail.com> wrote:
>
> Hi
>
> To answer your original question, the current alternatives to Int31 are 
> Uint63 (for unsigned primitive integers) and Sint63 (for signed primitive 
> integers).
>
> Best,
> Ana
>
> On Thu, 2 Dec 2021 at 23:14, mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> 
> wrote:
>>
>> Thank you very much Pierre and Xavier. It’s very helpful.
>>
>> Best,
>> Mukesh
>>
>> On Thu, 2 Dec 2021 at 8:17 pm, Xavier Leroy 
>> <xavier.leroy AT college-de-france.fr> wrote:
>>>
>>> On Thu, Dec 2, 2021 at 1:44 AM mukesh tiwari 
>>> <mukeshtiwari.iiitm AT gmail.com> wrote:
>>>>
>>>> I am looking for 16 bit unsigned integer library in Coq and I found this 
>>>> library [1] but at the very top it says, “This library has been 
>>>> deprecated since Coq version 8.10”, so I am curious about the other 
>>>> alternatives.
>>>>
>>>> One way, at the top of my head, I can do this by
>>>> Record UInt16 := mk_uint { val: N; 0 <= val < 2^16} and define all the 
>>>> needed functions and proofs but before that I would like see the 
>>>> existing solutions.
>>>
>>>
>>> The Integers library in CompCert implements this approach, for any number 
>>> of bits: https://compcert.org/doc/html/compcert.lib.Integers.html
>>>
>>> To get your 16-bit integers:
>>>
>>> Module Wordsize_16.
>>>   Definition wordsize := 16%nat.
>>>   Remark wordsize_not_zero: wordsize <> 0%nat.
>>>   Proof. unfold wordsize; congruence. Qed.
>>> End Wordsize_16.
>>>
>>> Module Int16 := Integers.Make(Wordsize_16).
>>>
>>> Enjoy,
>>>
>>> - Xavier Leroy
>>>
>>>
>>>>
>>>>
>>>> Best,
>>>> Mukesh
>>>>
>>>> [1] https://coq.inria.fr/library/Coq.Numbers.Cyclic.Int31.Int31.html