valid identifiers

Stream: new members

[Julian Berman]

Is there a place which says which unicode characters or categories are valid Lean identifiers? Just curious to notice e.g. Lean seems happy with variable {𝓘 : Type*} but not variable {𝐼 : Type*}

[Bryan Gin-ge Chen]

I think @Edward Ayers had a cheat sheet somewhere on GitHub but I can't find it now. I did find this Zulip post which might help.

[Julian Berman]

Aha thanks, that does help since me grepping the lean repo for the definition of token_kind::Identifier isn't helping.

[Edward Ayers]

https://github.com/EdAyers/edlib/blob/master/docs/unicode.md

[Edward Ayers]

not sure if it's still up to date

[Julian Berman]

@Edward Ayers amazing, thanks!

[Bryan Gin-ge Chen]

@Edward Ayers Thanks! Would you mind if we added that cheatsheet and maybe some of the other notes you wrote to the community website?

[Bryan Gin-ge Chen]

Or maybe we could just link to them, if you prefer.

[Julian Berman]

Heh -- @Edward Ayers "Not all JSON is javascript because of unicode issues." at least is fixed now.

[Julian Berman]

JSON is now a proper subset of Javascript

[Edward Ayers]

Hi Bryan, yeah sure do what you like with them! Although I wrote them mainly to get an idea of what is going on so they might contain misconceptions.

[Bryan Gin-ge Chen]

Thanks Ed! I created a GitHub issue for this. Anyone should feel free to take it on!