escaping `{` in interpolated strings

Stream: general

[Jason Gross]

Is there a way to get curly braces in interpolated strings? In python I'd write f"{{{foo}}}stuff" to get foo + "stuff", but this doesn't seem to work in Lean with s!"{{{foo}}}stuff"? And https://lean-lang.org/doc/reference/latest//Basic-Types/Strings/#string-interpolation doesn't seem to mention anything

[Eric Wieser]

s!"{foo}stuff" should mean the same thing as foo + "stuff"

[Jason Gross]

Oops, I meant to say that I wanted to know how to get "{" + foo + "}" + stuff

[Eric Wieser]

I guess{"{"} works

[Thomas Murrills]

s!"\{{foo}}stuff" works too, I believe (assuming you still want to interpolate foo, right?)

[Jason Gross]

Thank you! It seems that s!"\{{foo}}stuff works but the VSCode syntax highlighter doesn't highlight it correctly?

[Thomas Murrills]

Ooh, that's true...

For anyone who wants to see, here it is on web:

import Lean
run_cmd Lean.logInfo s!"\{{1+1}}"

image.png