How do we decipher the Lean4 documentation's ad hoc EBNF?

Stream: lean4

[Daniel Donnelly]

See this PASE post for more information about what I need, but basically, the EBNF used throughout the documentation for Lean4 is not making complete sense to me. So, any guidance would be appreciated.

I need to know more syntax than the small idiomatic subset of Lean4 that I do use. So, I'm going by the EBNF we have in the Lean4 docs. I can't really work with examples, since my PEGTL grammar auto-generator is quite mechanical and not very smart (no AI and/or grammar induction).

Specifically, what does the following mean more explicitly?

command ::= ...
    | deriving instance derivingClass,* for term,*

What does the first Kleene star apply to: is it (derivingClass ,)* or is it (deriving instance derivingClass ,)*?

Also, what do the "..." mean here? Perhaps it's related to the Kleene star list? My best guess is that it means include the other rules of Nonterminal "command", which can be found in other places of the docs.

[Patrick Massot]

The ... refers to all other commands defined elsewhere (def, theorem etc…). The derivingClass,* means “a comma separated list of derived classes”. So it could be Repr, ToString for instance.

[Robin Arnez]

The notation for syntax in the language reference is based off of the notation for syntax in Lean 4, so the documentation for syntax declarations also mostly applies to the syntax in the language reference: https://lean-lang.org/doc/reference/latest/Notations-and-Macros/Defining-New-Syntax/#syntax-rules (see Syntax Specifiers)

[Robin Arnez]

Concretely, the example means:
Among others, the keyword deriving followed by the keyword instance followed by a comma-separated list of syntax of kind derivingClass followed by the keyword for followed by a comma-separated list of syntax of kind term is a syntax of kind command.
Now, I'm aware, derivingClass is documented nowhere and there is no hover for it. However, all the syntax in the language reference is based off of Lean's syntax so you can find it here:

...
def derivingClass    := leading_parser
  optional ("@[" >> nonReservedSymbol "expose" >> "]") >> withForbidden "for" termParser
...

which reveals (written in Lean code rather than syntax notation) that derivingClass is an optional @[expose] before a term that may not contain the keyword for.

[Eric Paul]

I am confused about something in this example though, perhaps just a small mistake. The documentation says derivingClass,* but it appears that the implementation corresponds to derivingClass,+ (i.e. it uses sepBy1 and not sepBy).

The implementation of standalone deriving instances is here and that calls derivingClasses which uses sepBy1.

[Daniel Donnelly]

Thanks to all who posted to guide me. I will read through each post carefully in a few days. Currently working on GitManager / Tasks testing right now though.

[Daniel Donnelly]

Robin Arnez said:

Concretely, the example means:
Among others, the keyword deriving followed by the keyword instance followed by a comma-separated list of syntax of kind derivingClass followed by the keyword for followed by a comma-separated list of syntax of kind term is a syntax of kind command.
Now, I'm aware, derivingClass is documented nowhere and there is no hover for it. However, all the syntax in the language reference is based off of Lean's syntax so you can find it here:

...
def derivingClass    := leading_parser
  optional ("@[" >> nonReservedSymbol "expose" >> "]") >> withForbidden "for" termParser
...

which reveals (written in Lean code rather than syntax notation) that derivingClass is an optional @[expose] before a term that may not contain the keyword for.

Where did you get that the derivingClass (or the term?) may not contain the keyword "for"? Thanks! :cactus:

[Daniel Donnelly]

Actually, I found it it's done with Lean4 code. Will have to learn some more Lean4. So, I'm going through TPIL4 some more.