Different kinds of interpolated strings?

Stream: new members

[Kevin Cheung]

In the Lean 4 manual, interpolated strings such as s!"foo {bar}" are explained. But I have also seen things like m!"{term}" in HitchHiker Guide to Logical Verification and f!"{declName"} in Metaprogramming in Lean 4. Is there documentation that lists all such string literal prefixes and explains their meanings? Pointers greatly appreciated.

[Eric Wieser]

These notations are respectively

#check termS!_
#check Lean.termM!_
#check Std.termF!_

but unfortunately none of them have docstrings! If they did, then you would see that docstring when you hovered over them.

[Kevin Cheung]

Are these all?

[Eric Wieser]

Well, anyone can define a new one, but in practice those are the main ones you need

[Kevin Cheung]

I see. Thank you.