Zulip Chat Archive

Stream: new members

Topic: BNF for lean?


view this post on Zulip Francis Nixon (Jan 27 2019 at 12:33):

I was wondering there was a full BNF for lean somewhere. I noticed this: https://leanprover.github.io/reference/lexical_structure.html, but I seem to be unable to find a full grammar. Thank.

view this post on Zulip Mario Carneiro (Jan 27 2019 at 13:15):

The lean grammar isn't quite context free, at least in the expression part

view this post on Zulip Mario Carneiro (Jan 27 2019 at 13:16):

or rather, it's context free but the grammar can change depending on the commands that are read, and there are hooks for arbitrary computation in the parser

view this post on Zulip Mario Carneiro (Jan 27 2019 at 13:16):

But if you ignore all that you should be able to get a decent BNF


Last updated: May 08 2021 at 19:11 UTC