Topic: Keyword list
Logan Murphy (Nov 30 2020 at 15:02):
Is there somewhere I can find a list of reserved keywords? e.g.
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.
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
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:
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
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