BNF for lean?

Stream: new members

[Francis Nixon]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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