Zulip Chat Archive

Stream: new members

Topic: valid identifiers


view this post on Zulip 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*}

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Edward Ayers (Dec 24 2020 at 17:37):

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

view this post on Zulip Edward Ayers (Dec 24 2020 at 17:37):

not sure if it's still up to date

view this post on Zulip Julian Berman (Dec 24 2020 at 17:37):

@Edward Ayers amazing, thanks!

view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Dec 24 2020 at 17:40):

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

view this post on Zulip 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.

view this post on Zulip Julian Berman (Dec 24 2020 at 17:41):

JSON is now a proper subset of Javascript

view this post on Zulip 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.

view this post on Zulip 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