Zulip Chat Archive

Stream: new members

Topic: help debugging variables

Holly Liu (Aug 06 2021 at 18:15):

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

Yakov Pechersky (Aug 06 2021 at 18:57):

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 (Aug 06 2021 at 19:15):

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 (Aug 06 2021 at 21:58):

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 (Aug 06 2021 at 22:04):

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

Eric Wieser (Aug 06 2021 at 22:05):

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

Holly Liu (Aug 06 2021 at 22:23):

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

Eric Wieser (Aug 06 2021 at 22:29):

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:


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


Last updated: Dec 20 2023 at 11:08 UTC