Are "«" and "»" special characters?

Stream: new members

[Youngju Song]

I see these characters appearing here and there (e.g., when I use #check), wrapping namespaces, even though I haven't used these characters in my definition.
In my case, these characters doesn't seem to have any meaning: i.e., I can prove

example: «A».B = A.B := rfl

I am curious what they are and whether these characters are treated specially in Lean4.

[Damiano Testa]

They should serve as "escape" characters to produce a name, even when what you are typing may not be an name. For instance, I think that you can use them to make 3variable into a valid name. You can probably also use them to make \<<A.B\>> have a . "inside" the name, and not as segmentation for namespaces.

[Vlad Tsyrklevich]

Placing guillemets around a name, as in «Greeting», allow it to contain spaces or other characters that are normally not allowed in Lean names, and it allows reserved keywords such as if or def to be used as ordinary names by writing «if» or «def».

From FPIL

[Damiano Testa]

I had not realized that you could create fake name clashes with this:

theorem «A.B» : True := trivial

/-- error: unknown namespace 'A' -/
#guard_msgs in
open A

theorem A.B : True := trivial
open A

[Vlad Tsyrklevich]

I see that hovering over the guillemet in VS Code doesn't provide a helpful description, do we know where those hover texts live? I grep'd for the message for :: and couldn't find it in the vscode-lean4, lean4, or mathlib directories

[Kevin Buzzard]

Oh wow,

theorem «A.B» : True := trivial

theorem A.B : False := sorry

#check «A».«B» -- False
#check A.«B» -- False
#check «A.B» -- True

[Damiano Testa]

@Vlad Tsyrklevich does #find_syntax "\f<<"` tell you something useful? I'm on mobile and cannot test.

[Vlad Tsyrklevich]

It doesn't seem like #find_syntax is a known identifier in my local VS Code, even with import Mathlib?

[Damiano Testa]

It got merged recently: maybe you can try it in the online server?

[Vlad Tsyrklevich]

Indeed, it works on online. Found 948 uses among 2004 syntax declarations

[Damiano Testa]

Ouch: I need to add better filtering!

[Damiano Testa]

What if you place two consecutive guillemets?

[Vlad Tsyrklevich]

No hits, nor for f<<.

[Damiano Testa]

Ok, thanks! I'll have to look into this when I'm at a computer!

[Damiano Testa]

The closest that I could get to this is docs#Lean.Parser.ident, whose doc-string mentions the guillemets.

[Youngju Song]

@Damiano Testa @Vlad Tsyrklevich @Kevin Buzzard Thank you for the explanations!!

[Youngju Song]

The link to FPIL and Parser.ident is very helpful. I wish google search to be improved so that searching Lean4 "«" "»" would show these links on the top!