From 4afcc0aab0ce0939bca30fd3329f8d94844a7df4 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 25 Sep 2018 09:14:35 -0700
Subject: [PATCH] fix(library/init/lean/parser/term): do not allow mixing
 bracketed and unbracketed binders

---
 library/init/lean/expander.lean    |  7 ++++---
 library/init/lean/parser/term.lean | 12 ++++++------
 2 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean
index 1da8dc6976..4ed7208228 100644
--- a/library/init/lean/expander.lean
+++ b/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}
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index a0c8680b0c..cf2c310ddc 100644
--- a/library/init/lean/parser/term.lean
+++ b/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
 ]