Description of the parser?

Stream: lean4

[Tanner Swett]

Is there a document that describes how the Lean 4 parser works? I know that the parser prefers longer parses, and that the default associativity is... uh, I forget. But I have no idea what the algorithm actually does in order to obtain a parse tree.

[Mac Malone]

@Tanner Swett The header of Lean.Parser.Basic gives a high-level overview of the parser and docs#Lean.Parser.prattParser explains how specifically the precedence works.

[Tanner Swett]

Very nice, thank you!

It looks like the idea behind the parser is... neither terribly simple nor terribly complicated. I could probably get a good understanding of it given a few hours to puzzle stuff out.