batteries
batteries copied to clipboard
Fixed width signed integer datatypes.
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.
Would these support E or T division?
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.