Keyword list

Stream: general

[Logan Murphy]

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.

[Marc Huisinga]

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

[Marc Huisinga]

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]

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]

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