leanprover
chore: use ' instead of brackets for quotes
Bracket used for quoting an expression, such as (C ...) in
invalid {...} notation, {kind} type is not of the form (C ...){indentExpr type}
have been replaced by 'C ...'. This makes the messages clearer.
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):
- ✅ Mathlib branch lean-pr-testing-4464 has successfully built against this PR. (2024-06-16 11:49:08) View Log
Here both quotes are even used in the same error: https://github.com/leanprover/lean4/blob/0448e3f4ea1b2c476fc79aeee5d407971a1cd9e2/src/lake/Lake/Load/Package.lean#L31
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.
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?
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.
