feat: string gaps for continuing string literals across multiple lines #2821
Conversation
github-actions
bot
added
the
toolchain-available
|
kmill
force-pushed
the
string_gaps
branch
2 times, most recently
from
a17303d
to
d62eb06
Compare
kmill
changed the title
leanprover-community-mathlib4-bot
added
the
builds-mathlib
|
Implements RFC lean4#2838
For example,
```
"this is \
a string"
```
is equivalent to "this is a string".
|
Perfect test docs! I think all we're missing now is a changelog entry |
|
@Kha What are you looking for with the changelog entry? Do you mean I should write something in By the way, once the string literal PRs are all sorted out, I can write a rough draft of the strings section of the reference manual. |
Yes, a brief sentence similar to the PR title and a PR link are sufficent.
Great! You should probably get in touch with @david-christiansen for that. |
|
Until the reference manual project gets really underway early next year, I'm encouraging people to document what they're doing thoroughly, but with the understanding that it'll be substantially revised while integrating with the rest of the text. Any format is fine. Thanks! |
Implements "gaps" in string literals. These are escape sequences of the form
"\" newline whitespace+that have the interpretation of an empty string. For example,is equivalent to
"this is a string". These are modeled after string continuations in Rust.Implements RFC #2838