ASCII *not* allowed in constant names/identifiers?

Stream: new members

[Isak Colboubrani]

Lean allows a surprisingly wide range of characters in constant names (or identifiers in general).

Obviously whitespace—such as the space character (' '), tab ('\t'), and newline ('\n')—is banned, and the same goes for the ASCII control characters, but I'm sure there are other exclusions within the ASCII subset of Unicode.

What is the complete list of "printable"/non-control ASCII characters not permitted anywhere in an identifier/constant name?

[Isak Colboubrani]

Also, do the segments of an identifier wrapped in «…» receive any special parsing treatment? Some examples in the Lean code:

• «term_<||>_»
• Std.Sat.AIG.«term⟦_,_,_⟧»
• List.«term_<:+:_»

In other words, are those «…» quotes syntactically significant, or is it just a naming convention?

[Eric Wieser]

foo.«bar» is identical to foo.bar

[Eric Wieser]

But the former works when bar contains non-standard characters

[Isak Colboubrani]

Thanks! After some testing it seems like at least "#$%&()*+,-/:;<=>@[\]^`{|}~% are printable ASCII characters that are guaranteed to not be present in an identifier name except for when they are within «…» quotes (where anything goes). Perhaps that is the complete list.

[Isak Colboubrani]

Here’s a valid theorem name that pushes the «…» quoting to its limit and confuses the Zulip code formatter:

theorem « "#$%&()*+,-/:;<=>@[\]^`{|}~%» : True := trivial
#check « "#$%&()*+,-/:;<=>@[\]^`{|}~%»

[Jz Pan]

?, ! and ' are also valid without using «…».

Fun fact: it was possible to use «<script>...</script>» to inject javascript to doc page some time ago.

[Isak Colboubrani]

That's a nice point @Jz Pan, and the HTML-injection was clever! With the available options the most horrible looking yet valid ASCII-only theorem name should look something like this:

theorem _'!?.« "#$%&()*+,-/:;<=>@[\]^`{|}~%»._'!? : True := trivial
#check _'!?.« "#$%&()*+,-/:;<=>@[\]^`{|}~%»._'!?