[Merged by Bors] - fix(init/meta/interactive_base): Use }} in format
#650
Conversation
This way, escaped braces are balanced.
That is, `format!"a{{b}}c"` produces `"a{b}c"`, instead of
`format!"a{{b}c"`. Unbalanced braces are bad for editors and formatters,
so we should not encourage any syntax that requires unbalanced braces.
|
It seems like the only modules in mathlib this will obviously affect are in Mathlib seems to have its own version of |
|
I expect very few changes in mathlib. |
|
I agree with the balancing philosophy, and wholeheartedly approve of the whitespace formatting. bors r+ |
|
bors r+ |
As [discussed on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/curly.20braces/near/261185802). This way, escaped braces are balanced. That is, `format!"a{{b}}c"` produces `"a{b}c"`, instead of `format!"a{{b}c"`. Unbalanced braces are bad for editors and formatters, so we should not encourage any syntax that requires unbalanced braces.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
}} in format}} in format
As discussed on Zulip. This way, escaped braces are balanced. That is,
format!"a{{b}}c"produces"a{b}c", instead offormat!"a{{b}c". Unbalanced braces are bad for editors and formatters, so we should not encourage any syntax that requires unbalanced braces.