Errors in formal grammar of Function Binders

[nielsvoss]

Describe the bug

In the Function Binders box in 3.2.1.3. Implicit Functions: (sorry, couldn't figure out how to format this quote properly in GitHub)

Function binders may be identifiers:
funBinder ::= ...
| ident
sequences of identifiers with a type ascription:
funBinder ::= ...
| (ident ident* : term)
implicit parameters, with or without a type ascription:
funBinder ::= ...
| {ident*}
funBinder ::= ...
| {ident* : term}
instance implicits, anonymous or named:
funBinder ::= ...
| [term]
funBinder ::= ...
| [ident : term]
or strict implicit parameters, with or without a type ascription:
funBinder ::= ...
| ⦃(ident | hole)⦄
funBinder ::= ...
| ⦃ident* : term⦄

I think there are a couple mistakes.

1. It does not specify that you can surround vanilla identifiers with parentheses. example (x) (h : x = 2) ... is valid Lean code, yet it isn't permitted according to the BNF. (Of course, two levels of parentheses are not allowed, so example ((x)) (h : x = 2) ... is indeed an error, meaning that the single parentheses are a special case). Likewise, the ability to write (x y) is also missing.
2. The ability to write multiple terms in ⦃⦄ like ⦃x y⦄ is missing.
3. The BNF for curly brackets seems to suggest that {} and {: Nat} are valid function binders. The same is true for ⦃⦄
4. The ability to replace an identifier name with a hole is mentioned only for single ⦃⦄, although I don't see why it would be special for ⦃⦄. It is not mentioned for (), {}, or [], and it is also not mentioned for explicitly typed identifiers in ⦃⦄.
5. Double curly brackets ({{, }}) are not mentioned as alternatives to ⦃⦄ (although maybe this was intentional).
6. This isn't actually related to the Function Binders box, but the Functions with Varying Binders box seems to suggest that you can have a fun with no binders.

Demonstration

set_option autoImplicit false -- Just in case

-- The following are allowed in Lean, but not permitted according to the manual
-- Some parameters, like h₁, h₂, etc., exist to allow Lean to infer some types.
def ex1 (x) (h₁ : x = 0) : Unit := ()
def ex2 (x y) (h₁ : x = 0) (h₂ : y = "") : Unit := ()
def ex3 (_ : Nat) : Unit := ()
def ex4 (_) (h₁ : by rename_i x; exact x) : Unit := () -- tactic needed to get Lean to infer _'s type
def ex5 (_ : Nat) : Unit := ()
def ex6 {{x : Nat}} : Unit := () -- Grammar in manual never specifies that {{}} is allowed
def ex7 ⦃_ : Nat⦄ : Unit := ()
def ex8 ⦃x y⦄ (h₁ : x = 0) (h₂ : y = "") : Unit := ()

-- The following are allowed according to the manual, but are illegal in Lean
def ex9 {} : Unit := ()
def ex10 {: Nat} : Unit := ()
def ex11 ⦃: Nat⦄ : Unit := ()
def ex12 : Unit → Unit := fun => ()

[david-christiansen]

Thanks - when I fix this, I'll adopt your tests as well.