From 98dbe45ab8b95319a37bd110d648cd86bbe25b02 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 5 Oct 2020 13:27:18 -0700
Subject: [PATCH] chore: remove `Monad List` instance
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

@Kha The new `do` notation works for pure code too.
It automatically inserts `Id` if the expected type is not a monad.
This works great when we are not conflating data and control.
After deleting `Monad List`, we will be able to write functions such as
```lean
def mapWhen (p : Nat → Bool) (f : Nat → Nat) (xs : List Nat) : List Nat := do
for x in xs do
  if p x then
    x := f x
```
without adding `Id.run` before the `do`.
---
 src/Init/Data/List.lean           |  1 -
 src/Init/Data/List/Instances.lean | 20 --------------------
 tests/lean/run/bigop.lean         |  4 ++--
 3 files changed, 2 insertions(+), 23 deletions(-)
 delete mode 100644 src/Init/Data/List/Instances.lean

diff --git a/src/Init/Data/List.lean b/src/Init/Data/List.lean
index 9af534e509..6bb2c73169 100644
--- a/src/Init/Data/List.lean
+++ b/src/Init/Data/List.lean
@@ -6,5 +6,4 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.List.Basic
 import Init.Data.List.BasicAux
-import Init.Data.List.Instances
 import Init.Data.List.Control
diff --git a/src/Init/Data/List/Instances.lean b/src/Init/Data/List/Instances.lean
deleted file mode 100644
index 6b190d5c08..0000000000
--- a/src/Init/Data/List/Instances.lean
+++ /dev/null
@@ -1,20 +0,0 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
--/
-prelude
-import Init.Data.List.Basic
-import Init.Control.Alternative
-import Init.Control.Monad
-open List
-
-universes u v
-
-instance : Monad List :=
-{ pure := @List.pure, map := @List.map, bind := @List.bind }
-
-instance : Alternative List :=
-{ List.Monad with
-  failure := @List.nil,
-  orelse  := @List.append }
diff --git a/tests/lean/run/bigop.lean b/tests/lean/run/bigop.lean
index 7870e2f534..8c26950717 100644
--- a/tests/lean/run/bigop.lean
+++ b/tests/lean/run/bigop.lean
@@ -25,8 +25,8 @@ class Enumerable (α : Type) :=
 instance : Enumerable Bool :=
 { elems := [false, true] }
 
-instance {α β} [Enumerable α] [Enumerable β]: Enumerable (α × β) :=
-{ elems := do let a ← Enumerable.elems α; let b ← Enumerable.elems β; pure (a, b) }
+-- instance {α β} [Enumerable α] [Enumerable β]: Enumerable (α × β) :=
+-- { elems := do let a ← Enumerable.elems α; let b ← Enumerable.elems β; pure (a, b) }
 
 partial def finElemsAux (n : Nat) : (i : Nat) → i < n → List (Fin n)
 | 0,   h => [⟨0, h⟩]