-
Notifications
You must be signed in to change notification settings - Fork 50
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
ExprKind::NeverToAny
=> Term::Absurd
=> Invalid Why3
#972
Comments
Something like |
I don't think this has to do with |
Hmmm, yea but that's still incorrect in why3; we should generate |
I don't think we should generated |
Yea that's better than |
When running CI for the Prusti translation I noticed that
absurd
seem to no longer be validWhy3
, but it still can get generated from the THIR never to any expression eg.The text was updated successfully, but these errors were encountered: