-
Notifications
You must be signed in to change notification settings - Fork 22
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
Library extensions #1235
base: main
Are you sure you want to change the base?
Library extensions #1235
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks fine to me. Inserting arithmetic operations symbols only for integers seems like a good change, we will avoid the F* type errors for other types that implement the Rust traits for arithmetic operators.
@karthikbhargavan please update and fix ci issues to get this merged |
This is still not working correctly. Not ready. |
This one hit some problems with the engine changes. We will try to split apart the library changes to get them in first. |
This PR does two things.
Library extensions
It adds elements to the F* proof library that were needed in PQ11 and Bertie.
These are yet another motivation for having a complete core library
Operators
It changes the way we compile operators to F*
Currently, all arithmetic operators are translated to the integer operators (+., -., etc.) even if these operators were defined using trait implementations for non-arithmetic types, which results in type errors in F*.
This PR specialized the treatment of booleans and integers, and leaves the rest as typeclass implementations.
This is still not the most general treatment possible, but attempts to do just enough for the examples we have currently.