lexical rules

Stream: lean4

[Roland Leißa]

Hi all, I'm pretty sure I found somewhere the exact lexical rules of Lean4 with all the crazy unicode specs etc but I can't find it anymore. Does somebody know where I can find it?

[Henrik Böving]

Lean can extend its own syntax dynamically, you won't be able to find a closed reference for its syntax. At best (potentially large) fragments of it

[Roland Leißa]

I know that. But I was asking for the lexical rules - not the syntactical ones.

[Roland Leißa]

Ah, I think the document I found was from Lean3:
https://leanprover.github.io/reference/lexical_structure.html

Does somebody know how much has changed in Lean4 now with all the syntax extesions?

[Kyle Miller]

There's one for Lean 4, but it's not necessarily up-to-date: https://github.com/leanprover/lean4/blob/master/doc/lexical_structure.md

[Roland Leißa]

Thanks, Kyle. This is what I was looking for.