Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fixed width signed integer datatypes. #472

Open
joehendrix opened this issue Dec 20, 2023 · 2 comments
Open

Fixed width signed integer datatypes. #472

joehendrix opened this issue Dec 20, 2023 · 2 comments

Comments

@joehendrix
Copy link
Contributor

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
Copy link
Collaborator

Would these support E or T division?

@digama0
Copy link
Member

digama0 commented Feb 20, 2024

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants