From e29bf35d15cb89445e074e94f5bc902daf0c8f1d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 2 Jul 2019 11:01:05 -0700
Subject: [PATCH] chore(frontends/lean/builtin_exprs): remove hard coded `(::)`
 notation

---
 library/init/control/combinators.lean |  2 +-
 library/init/data/array/basic.lean    |  2 +-
 src/frontends/lean/builtin_exprs.cpp  | 23 -----------------------
 3 files changed, 2 insertions(+), 25 deletions(-)

diff --git a/library/init/control/combinators.lean b/library/init/control/combinators.lean
index fee15d0188..b216228dac 100644
--- a/library/init/control/combinators.lean
+++ b/library/init/control/combinators.lean
@@ -60,7 +60,7 @@ namespace List
 @[specialize]
 def mmap {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
 | []      := pure []
-| (a::as) := (::) <$> (f a) <*> mmap as
+| (a::as) := List.cons <$> (f a) <*> mmap as
 
 @[specialize]
 def mfor {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit
diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean
index 97d8179848..4f50a40a40 100644
--- a/library/init/data/array/basic.lean
+++ b/library/init/data/array/basic.lean
@@ -248,7 +248,7 @@ revIterateAux a f a.size (Nat.leRefl _) b
 revIterate a b (λ _, f)
 
 def toList (a : Array α) : List α :=
-a.revFoldl [] (::)
+a.revFoldl [] List.cons
 
 instance [HasRepr α] : HasRepr (Array α) :=
 ⟨repr ∘ toList⟩
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index a12c61f46a..aff3579b5b 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -768,28 +768,6 @@ static expr parse_lparen(parser & p, unsigned, expr const *, pos_info const & po
     }
 }
 
-static expr parse_lambda_cons(parser & p, unsigned, expr const *, pos_info const & pos) {
-    list<pair<transition, parse_table>> ts = p.led().find(get_dcolon_tk());
-    if (!ts || tail(ts) || !head(ts).second.is_accepting())
-        throw parser_error("invalid '(::)' notation, infix operator '::' has not been defined yet or is the prefix of another notation declaration", pos);
-    notation::action const & act = head(ts).first.get_action();
-    if (act.kind() != notation::action_kind::Expr)
-        throw parser_error("invalid '(::)' notation, declaration for operator '::' is not compatible with the `(::)` syntactic sugar", pos);
-    expr args[2];
-    buffer<expr> vars;
-    args[0] = mk_local(p.next_name(), "_x", mk_expr_placeholder(), mk_binder_info());
-    vars.push_back(args[0]);
-    args[1] = mk_local(p.next_name(), "_y", mk_expr_placeholder(), mk_binder_info());
-    vars.push_back(args[1]);
-    buffer<expr> cs;
-    for (notation::accepting const & acc : head(ts).second.is_accepting()) {
-        expr r = p.copy_with_new_pos(acc.get_expr(), pos);
-        r = p.save_pos(mk_infix_function(Fun(vars, instantiate_rev(r, 2, args), p)), pos);
-        cs.push_back(r);
-    }
-    return p.save_pos(mk_choice(cs.size(), cs.data()), pos);
-}
-
 static expr parse_inaccessible(parser & p, unsigned, expr const *, pos_info const & pos) {
     expr e = p.parse_expr();
     if (!p.in_pattern()) {
@@ -847,7 +825,6 @@ parse_table init_nud_table() {
     r = r.add({transition("`", mk_ext_action(parse_quoted_name))}, x0);
     // r = r.add({transition("(:", Expr), transition(":)", mk_ext_action(parse_pattern))}, x0);
     r = r.add({transition("()", mk_ext_action(parse_unit))}, x0);
-    r = r.add({transition("(::)", mk_ext_action(parse_lambda_cons))}, x0);
     r = r.add({transition("fun", mk_ext_action(parse_lambda))}, x0);
     r = r.add({transition("Pi", Binders), transition(",", mk_scoped_expr_action(x0, 0, false))}, x0);
     r = r.add({transition("Type", mk_ext_action(parse_Type))}, x0);