Zulip Chat Archive

Stream: general

Topic: parsing technology


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Assia Mahboubi (Jun 08 2018 at 12:33):

Thanks a lot @Sebastian Ullrich !


Last updated: May 13 2021 at 20:13 UTC