parsing technology

Stream: general

[Assia Mahboubi]

Hi there, can someone help me finding the code of Lean's parser and/or its documentation?

[Sebastian Ullrich]

Hi Assia. There is basically no documentation - this should certainly change for Lean 4 where the parser will be rewritten in Lean to be user-accessible. The current one is implemented in C++ as a recursive-descent LL(1) Pratt parser - https://github.com/leanprover/lean/blob/master/src/frontends/lean/parser.h

[Assia Mahboubi]

Thanks a lot @Sebastian Ullrich !