-
Notifications
You must be signed in to change notification settings - Fork 345
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
chore: use ' instead of brackets for quotes #4464
base: master
Are you sure you want to change the base?
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.
It's good to be consistent, but probably subjective which variant is clearer. I'd be curious what @david-christiansen will say.
Also, do we maybe use back ticks in some places as well?
Yeah, I wasn't sure about backticks vs single quotes. I went for normal quotes because they seem to be used more than backticks. I don't know of any difference in the meaning between the two. |
Mathlib CI status (docs):
|
Here both quotes are even used in the same error: lean4/src/lake/Lake/Load/Package.lean Line 31 in 0448e3f
|
My impression, from looking at the lines of code in the diffs, is that single ticks are used to refer to a names and parentheses or backticks to quote expressions. Such semantic differentiation might actually be intended and useful, but then should be documented for the other developers so that we can apply them consistently. |
Me too. I feel like we are not using quotes and backticks consistently in error messages and doc-strings. I am also curious about what @david-christiansen will say. We should document the decision, and start enforcing from now on. |
Bracket used for quoting an expression, such as (C ...) in
have been replaced by 'C ...'. This makes the messages clearer.