fix(library/init/lean/parser/term): do not allow mixing bracketed and unbracketed binders

library/init/lean/expander.lean

@@ -32,6 +32,9 @@ instance coe_ident_term_ident : has_coe parser.ident.view term.ident.view :=
 instance coe_term_ident_binder_id : has_coe term.ident.view binder_id.view :=
 ⟨binder_id.view.id⟩
 
+instance coe_binders {α : Type} [has_coe_t α binder_id.view] : has_coe (list α) term.binders.view :=
+⟨λ ids, binders.view.unbracketed {ids := ids.map coe}⟩
+
 def mixfix.transform : transformer :=
 λ stx, do
   let v := view mixfix stx,
@@ -48,9 +51,7 @@ def mixfix.transform : transformer :=
             transition := some $ transition.view.arg {
               id := `b,
               action := prec_to_action <$> quoted.prec}}]},
-        review lambda {binders := [
-            binder.view.unbracketed {ids := [`b]}
-          ],
+        review lambda {binders := [`b],
           body := review app {fn := v.term, arg := review term.ident `b}})
      | _ := none) | pure stx,
    pure $ review «notation» {spec := spec, term := term}

library/init/lean/parser/term.lean

@@ -110,10 +110,10 @@ node_choice! bracketed_binder {
 }
 
 @[derive has_tokens has_view]
-def binder.parser : term_parser :=
-node_choice! binder {
-  bracketed: bracketed_binder.parser,
-  unbracketed: binder_content.parser
+def binders.parser : term_parser :=
+node_choice! binders {
+  bracketed: bracketed_binder.parser+,
+  unbracketed: binder_content.parser,
 }
 
 end binder
@@ -122,7 +122,7 @@ end binder
 def lambda.parser : term_parser :=
 node! lambda [
   op: unicode_symbol "λ" "fun" max_prec,
-  binders: binder.parser+,
+  binders: binders.parser,
   ",",
   body: recurse 0
 ]
@@ -131,7 +131,7 @@ node! lambda [
 def pi.parser : term_parser :=
 node! pi [
   op: unicode_symbol "Π" "Pi" max_prec,
-  binders: binder.parser+,
+  binders: binders.parser,
   ",",
   range: recurse 0
 ]