help debugging

Stream: new members

[Holly Liu]

i get the unexpected tokenerror when hovering over the red line:
image.png
how do i go about this?

[Mario Carneiro]

try restarting lean, try deleting and rewriting the characters in that area in case there are some hidden bad unicode characters

[Mario Carneiro]

try not using unicode names (at least for debugging purposes)

[Holly Liu]

i tried those and it looks like σⱼ doesn't work for me at all, although other subscripts like σₖ seem to work.

[Mario Carneiro]

Oh unicode. Of course it would be the case that subscript i is in the Phonetic extensions block, subscript j is in the Latin Extended-C block, and subscript k is in the Superscripts and subscripts block.

[Mario Carneiro]

unfortunately lean's list of subscript blocks in unicode missed a spot

[Mario Carneiro]

If you really want to use a non-identifier character in an identifier, you can enclose it in "french double quotes":

example («σⱼ» : ℕ) : ℕ := «σⱼ»

[Mario Carneiro]

or you can just get lazy and use σ_j or σj

[Holly Liu]

ok. very sad that i can't do the usual i,j indexing.

[Holly Liu]

sorry if this is a dumb question. lean isn't able to find the σᵢ all the way at the bottom here although i defined it in braid_rels
image.png

[Holly Liu]

it's also the unexpected token error

[Mario Carneiro]

I think subscript i has the same problem