is quoted identifier still available in lean4

Stream: lean4

[Hsin-Po Wang]

It seems in lean 3 I can say theorem x is 10 and I get a theorem whose name is "x is 10" with all the spaces. Is this syntax still available in lean4? I can't find the counter part in lean 4 document not can I find a statement that this is deprecated.

[Kim Morrison]

Look for "French quotes"

[Robin Arnez]

\f<<>>

[Robin Carlier]

Grepping the reference manual for "french" or "French" gives no hit. Grepping for "«" gives hits but none seems to be actually documenting the feature. Am I doing it wrong or is this a hole in the manual?

[Simon Dima]

https://lean-lang.org/doc/reference/latest///////////////Source-Files-and-Modules/#--tech-term-guillemets
Seems to be the doc in question

[Robin Carlier]

Oh, then I was just doing it wrong! ( yep, I overlooked one of the hit for "«")

[Ruben Van de Velde]

That's a lot of slashes!

[Mario Carneiro]

#general > Lean Reference search bar adding "/" characters to URL @ 💬

[Hsin-Po Wang]

beautiful! Thanks all.

[Kyle Miller]

This feature is the same as it was in Lean 3.

Hsin-Po Wang said:

It seems in lean 3 I can say theorem x is 10

Can you give an example of what you mean here? What's a Lean 3 example that worked and what wasn't working in Lean 4?