-
Notifications
You must be signed in to change notification settings - Fork 58
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
Const members of an enum #1107
Comments
Try This may be a syntax inconsistency we may want to fix (in functions, exec is the default). |
Thank you! Yes, it works with a |
related (but slightly different) (but probably same root cause): #861 |
Ah I see. Right, makes sense. This is indeed probably a bug (or a missing part of a feature). The bug @tjhance refers to is indeed likely another symptom of the same cause (thanks for looking it up!). |
A workaround for having the same const in spec and exec but not being able to declare it using the syntax above is to use
Not sure if this is intended functionality, but it seems to work for me, in case it turns out that having the dual-mode functionality is unsound in some way. |
I have the following code (playground link):
This gives me the following error message:
I am confused by this error message. Why is
Mode::A
inferred to have modespec
here? My understanding was that after #843, constant declarations should be dual-mode exec and spec.(Not sure if this is an actual bug in Verus or there's just some syntax I am missing!)
The text was updated successfully, but these errors were encountered: