-
-
Notifications
You must be signed in to change notification settings - Fork 40
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
[FEATURE] Change the format of uninterpreted constants #1130
Labels
Comments
This is a purely usability feature. @Kukovec what do you think? |
I have no strong attachments to either syntax, if you like this one more we can easily change it. |
konnov
added a commit
that referenced
this issue
Dec 2, 2021
…onstants-naming Closes #1130: Improve the format of uninterpreted constants to name_OF_TYPE
thpani
added a commit
that referenced
this issue
Feb 9, 2022
thpani
added a commit
that referenced
this issue
Feb 9, 2022
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
In the current format, we have to write uninterpreted constants as
uval_TYPE_name
, e.g.:/\ tmState = "uval_SORT_STATE_init"
See TwoPhaseUFO for more examples.
I find the current notation to be verbose and hard to read. I am proposing to change it to the more readable format:
So the above example would look like follows:
/\ tmState = "init_OF_SORT_STATE"
The benefit of this new format is that the most important part of the constant appears on the left, that is,
init
. Moreover, the type and the infix_OF_
are both capitalized, and they appear on the right, which is more convenient to type and read. It is also more consistent with our type annotations.The text was updated successfully, but these errors were encountered: