-
Notifications
You must be signed in to change notification settings - Fork 63
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
Add support for translating Cryptol constraint guards #1911
Conversation
Closes #1897. This change adds support for translating Cryptol constraint guards into nested if-then-else expressions so that they may be reasoned about in SAW.
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 good overall! Just some small issues with the comments / documentation
Co-authored-by: Ryan Scott <[email protected]>
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.
Great stuff! Do mention these changes in the SAW changelog, since they're a user-facing feature. Otherwise, LGTM.
Closes #1897.
This change adds support for translating Cryptol constraint guards into nested if-then-else expressions so that they may be reasoned about in SAW.