## Stream: new members

### Topic: valid identifiers

#### Julian Berman (Dec 24 2020 at 17:32):

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 (Dec 24 2020 at 17:35):

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 (Dec 24 2020 at 17:37):

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

#### Edward Ayers (Dec 24 2020 at 17:37):

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

#### Edward Ayers (Dec 24 2020 at 17:37):

not sure if it's still up to date

#### Julian Berman (Dec 24 2020 at 17:37):

@Edward Ayers amazing, thanks!

#### Bryan Gin-ge Chen (Dec 24 2020 at 17:40):

@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 (Dec 24 2020 at 17:40):

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

#### Julian Berman (Dec 24 2020 at 17:41):

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

#### Julian Berman (Dec 24 2020 at 17:41):

JSON is now a proper subset of Javascript

#### Edward Ayers (Dec 27 2020 at 13:18):

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 (Dec 28 2020 at 17:22):

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

Last updated: May 10 2021 at 00:31 UTC