Lean 4 Parser

Stream: lean4 dev

[Kali]

Hello! I'm building a proof assistant as a learning project and am wondering how Lean implements user-defined notation. Is the program parsed and elaborated simultaneously? Or maybe the notation commands are parsed first and then the rest of the file? Any and all details are appreciated!

[Mario Carneiro]

the file is parsed one command at a time, and the command may change the parser to be used in the following command. In particular, you cannot affect the parsing of the command in the middle of parsing (which you wouldn't think is a requested feature, but does come up when e.g. declaring a notation inside a scope).

[Kali]

Makes sense, thanks!