help debugging variables

Stream: new members

[Holly Liu]

is there a way to do σᵢ but with i+1 as the subscript?

[Yakov Pechersky]

There is nothing magical about subscripts. They are just sequences of letters. You could name your variables sigma_i_plus_one and that would have as much (or as little) meaning as σᵢ₊₁

[Eric Wieser]

For questions like this, there are really only three things to consider:

• Can the thing you're asking for be typed in unicode plaintext? This is not a lean question, but lean users might know more about unicode maths than most other mathematicians. There are tools online that let you draw a character and find the closest unicode character (shapecatcher.com)
• Does the vscode extension have a shortcut for your chosen character. If no, ask for one, or PR it yourself!
• Is the character you choose valid in an identifier name? If it's not, then it's probably still valid as part of notation.

[Holly Liu]

does it need to be a shortcut in order to be recognized by lean? currently i get the error unexpected token when typing σᵢ₊₁

[Eric Wieser]

The character has to match the regex [_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟0-9'ⁿ-₉ₐ-ₜᵢ-ᵪ].

[Eric Wieser]

That is, it has to lie in one of the A-Z ranges between the square bracket (every character has a number)

[Holly Liu]

does that mean it can't be a combination of characters from different ranges?

[Eric Wieser]

No, it can be any mix of characters from all ranges - although the first character of each identifier is slightly more strict. The regex vscode actually uses to highlight is here:

https://github.com/leanprover/vscode-lean/blob/2b43982c4c6305a0f20f156152a60613a6f1a683/syntaxes/lean.json#L183-L190

While the actual C code that determines once and for all whether a name is valid is here:

https://github.com/leanprover-community/lean/blob/65ad4ffdb3abac75be748554e3cbe990fb1c6500/src/util/name.cpp#L28-L56