search

leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover
Apache License 2.0
250 stars 104 forks source link

Fixed width signed integer datatypes. #472

Open joehendrix opened 11 months ago

joehendrix commented 11 months ago

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.

fgdorais commented 9 months ago

Would these support E or T division?

digama0 commented 9 months ago

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.

dwrensha commented 1 week ago

Fixed width signed integers have landed in core: https://github.com/leanprover/lean4/issues/3162#issuecomment-2457964425