You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
Lean should provide
Int8
,Int16
,Int32
andInt64
to complementUInt8
,UInt16
,UInt32
, andUInt64
.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.
The text was updated successfully, but these errors were encountered: