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⟩]