batteries icon indicating copy to clipboard operation
batteries copied to clipboard

Fixed width signed integer datatypes.

Open joehendrix opened this issue 1 year ago • 2 comments

Lean should provide Int8, Int16, Int32 and Int64 to complement UInt8, UInt16, UInt32, and UInt64.

Ideally the definitions should be in core and the compiler extended to generate efficient code for them, but Std may need to provide additional lemma support.

joehendrix avatar Dec 20 '23 19:12 joehendrix

Would these support E or T division?

fgdorais avatar Feb 20 '24 03:02 fgdorais

Hopefully the official division definition will switch to E division soon, it recently moved to core so I think it's just a matter of swapping the names around and finally being able to remove the confusion about ediv theorems. I would expect both divisions to be available, but given that Int is using E division now I think / should perform E division on signed integer types.

digama0 avatar Feb 20 '24 14:02 digama0