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: May 13 2021 at 20:13 UTC