Zulip Chat Archive

Stream: general

Topic: parsing technology

Assia Mahboubi (Jun 08 2018 at 12:06):

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

Sebastian Ullrich (Jun 08 2018 at 12:24):

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 (Jun 08 2018 at 12:33):

Thanks a lot @Sebastian Ullrich !

Last updated: Dec 20 2023 at 11:08 UTC