Zulip Chat Archive

Stream: general

Topic: Keyword list


view this post on Zulip Logan Murphy (Nov 30 2020 at 15:02):

Is there somewhere I can find a list of reserved keywords? e.g. lemma def inductive. I can see some of the when I run #print notation but I'm assuming there's a hardcoded list somewhere, I just can't seem to find it.

view this post on Zulip Marc Huisinga (Nov 30 2020 at 15:05):

this is very likely not up to date with current community lean, but: https://leanprover.github.io/reference

view this post on Zulip Marc Huisinga (Nov 30 2020 at 15:06):

i'm not sure if section 4 and 5 are exhaustive for an older version of lean either, but it's a good start :sweat_smile:

view this post on Zulip Floris van Doorn (Nov 30 2020 at 20:42):

I don't know if this list is complete, but here is a list: https://github.com/leanprover-community/lean/blob/f53f52b78651d9e114a73ef6f3fcb971f7ada978/src/frontends/lean/token_table.cpp#L79-L122

view this post on Zulip Logan Murphy (Dec 01 2020 at 13:48):

Thank you Floris, that's exactly what I was looking for!


Last updated: May 10 2021 at 19:16 UTC