diff --git a/library/init/bool.lean b/library/init/bool.lean
index 1661b783fc..2b21aeaa04 100644
--- a/library/init/bool.lean
+++ b/library/init/bool.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 prelude
-import init.datatypes
+import init.core
 
 @[inline] def {u} cond {A : Type u} : bool → A → A → A
 | tt a b := a
diff --git a/library/init/collection.lean b/library/init/collection.lean
deleted file mode 100644
index 908262f5b9..0000000000
--- a/library/init/collection.lean
+++ /dev/null
@@ -1,54 +0,0 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.logic
-universe variables u v
-
-/- Type class used to implement polymorphic notation for collections.
-   Example: {a, b, c}. -/
-class insertable (A : Type u) (C : Type u → Type v) :=
-(empty : C A) (insert : A → C A → C A)
-
-section
-variables {A : Type u} {C : Type u → Type v}
-variable [insertable A C]
-
-def insert : A → C A → C A :=
-insertable.insert
-
-/- The empty collection -/
-def empty_col : C A :=
-insertable.empty A C
-
-notation `∅` := empty_col
-
-def singleton (a : A) : C A :=
-insert a ∅
-end
-
-/- Type class used to implement the notation [ a ∈ c | p a ] -/
-class decidable_separable (A : Type u) (C : Type u → Type v) :=
-(sep : ∀ (p : A → Prop) [decidable_pred p], C A → C A)
-
-section
-variables {A : Type u} {C : Type u → Type v}
-variable [decidable_separable A C]
-
-def dec_sep (p : A → Prop) [decidable_pred p] : C A → C A :=
-decidable_separable.sep p
-end
-
-/- Type class used to implement the notation { a ∈ c | p a } -/
-class separable (A : Type u) (C : Type u → Type v) :=
-(sep : (A → Prop) → C A → C A)
-
-section
-variables {A : Type u} {C : Type u → Type v}
-variable [separable A C]
-
-def sep : (A → Prop) → C A → C A :=
-separable.sep
-end
diff --git a/library/init/datatypes.lean b/library/init/core.lean
similarity index 66%
rename from library/init/datatypes.lean
rename to library/init/core.lean
index b06d33f6d7..d3a70da540 100644
--- a/library/init/datatypes.lean
+++ b/library/init/core.lean
@@ -3,7 +3,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 
-Basic datatypes and notation
+notation, basic datatypes and type classes
 -/
 prelude
 
@@ -11,6 +11,73 @@ notation `Prop`  := Type 0
 notation `Type₂` := Type 2
 notation `Type₃` := Type 3
 
+/- Logical operations and relations -/
+
+reserve prefix `¬`:40
+reserve prefix `~`:40
+reserve infixr ` ∧ `:35
+reserve infixr ` /\ `:35
+reserve infixr ` \/ `:30
+reserve infixr ` ∨ `:30
+reserve infix ` <-> `:20
+reserve infix ` ↔ `:20
+reserve infix ` = `:50
+reserve infix ` ≠ `:50
+reserve infix ` ≈ `:50
+reserve infix ` ~ `:50
+reserve infix ` ≡ `:50
+reserve infixl ` ⬝ `:75
+reserve infixr ` ▸ `:75
+reserve infixr ` ▹ `:75
+
+/- types and type constructors -/
+
+reserve infixr ` ⊕ `:30
+reserve infixr ` × `:35
+
+/- arithmetic operations -/
+
+reserve infixl ` + `:65
+reserve infixl ` - `:65
+reserve infixl ` * `:70
+reserve infixl ` / `:70
+reserve infixl ` % `:70
+reserve prefix `-`:100
+reserve infix ` ^ `:80
+
+reserve infixr ` ∘ `:90                 -- input with \comp
+
+reserve infix ` <= `:50
+reserve infix ` ≤ `:50
+reserve infix ` < `:50
+reserve infix ` >= `:50
+reserve infix ` ≥ `:50
+reserve infix ` > `:50
+
+/- boolean operations -/
+
+reserve infixl ` && `:70
+reserve infixl ` || `:65
+
+/- set operations -/
+
+reserve infix ` ∈ `:50
+reserve infix ` ∉ `:50
+reserve infixl ` ∩ `:70
+reserve infixl ` ∪ `:65
+reserve infix ` ⊆ `:50
+reserve infix ` ⊇ `:50
+reserve infix ` ⊂ `:50
+reserve infix ` ⊃ `:50
+reserve infix `\`:70
+
+/- other symbols -/
+
+reserve infix ` ∣ `:50
+reserve infixl ` ++ `:65
+reserve infixr ` :: `:67
+reserve infixl `; `:1
+
 universe variables u v
 
 inductive poly_unit : Type u
@@ -26,6 +93,9 @@ inductive false : Prop
 
 inductive empty : Type
 
+def not (a : Prop) := a → false
+prefix `¬` := not
+
 inductive eq {A : Type u} (a : A) : A → Prop
 | refl : eq a
 
@@ -92,6 +162,22 @@ inductive bool : Type
 | ff : bool
 | tt : bool
 
+class inductive decidable (p : Prop)
+| is_false : ¬p → decidable
+| is_true :  p → decidable
+
+@[reducible]
+def decidable_pred {A : Type u} (r : A → Prop) :=
+Π (a : A), decidable (r a)
+
+@[reducible]
+def decidable_rel {A : Type u} (r : A → A → Prop) :=
+Π (a b : A), decidable (r a b)
+
+@[reducible]
+def decidable_eq (A : Type u) :=
+decidable_rel (@eq A)
+
 inductive option (A : Type u)
 | none {} : option
 | some    : A → option
@@ -109,43 +195,85 @@ inductive nat
 
 /- Declare builtin and reserved notation -/
 
-class has_zero   (A : Type u) := (zero : A)
-class has_one    (A : Type u) := (one : A)
-class has_add    (A : Type u) := (add : A → A → A)
-class has_mul    (A : Type u) := (mul : A → A → A)
-class has_inv    (A : Type u) := (inv : A → A)
-class has_neg    (A : Type u) := (neg : A → A)
-class has_sub    (A : Type u) := (sub : A → A → A)
-class has_div    (A : Type u) := (div : A → A → A)
-class has_dvd    (A : Type u) := (dvd : A → A → Prop)
-class has_mod    (A : Type u) := (mod : A → A → A)
-class has_le     (A : Type u) := (le : A → A → Prop)
-class has_lt     (A : Type u) := (lt : A → A → Prop)
-class has_append (A : Type u) := (append : A → A → A)
-class has_andthen(A : Type u) := (andthen : A → A → A)
+class has_zero     (A : Type u) := (zero : A)
+class has_one      (A : Type u) := (one : A)
+class has_add      (A : Type u) := (add : A → A → A)
+class has_mul      (A : Type u) := (mul : A → A → A)
+class has_inv      (A : Type u) := (inv : A → A)
+class has_neg      (A : Type u) := (neg : A → A)
+class has_sub      (A : Type u) := (sub : A → A → A)
+class has_div      (A : Type u) := (div : A → A → A)
+class has_dvd      (A : Type u) := (dvd : A → A → Prop)
+class has_mod      (A : Type u) := (mod : A → A → A)
+class has_le       (A : Type u) := (le : A → A → Prop)
+class has_lt       (A : Type u) := (lt : A → A → Prop)
+class has_append   (A : Type u) := (append : A → A → A)
+class has_andthen  (A : Type u) := (andthen : A → A → A)
+class has_union    (A : Type u) := (union : A → A → A)
+class has_inter    (A : Type u) := (inter : A → A → A)
+class has_sdiff    (A : Type u) := (sdiff : A → A → A)
+class has_subset   (A : Type u) := (subset : A → A → Prop)
+class has_ssubset  (A : Type u) := (ssubset : A → A → Prop)
+/- Type class used to implement polymorphic notation for collections.
+   Example: {a, b, c}. -/
+class insertable (A : Type u) (C : Type u → Type v) :=
+(empty : C A) (insert : A → C A → C A)
+/- Type class used to implement the notation { a ∈ c | p a } -/
+class separable (A : Type u) (C : Type u → Type v) :=
+(sep : (A → Prop) → C A → C A)
+/- Type class for set-like membership -/
+class has_mem (A : Type u) (C : Type u → Type v) := (mem : A → C A → Prop)
 
-def zero    {A : Type u} [has_zero A]    : A            := has_zero.zero A
-def one     {A : Type u} [has_one A]     : A            := has_one.one A
-def add     {A : Type u} [has_add A]     : A → A → A    := has_add.add
-def mul     {A : Type u} [has_mul A]     : A → A → A    := has_mul.mul
-def sub     {A : Type u} [has_sub A]     : A → A → A    := has_sub.sub
-def div     {A : Type u} [has_div A]     : A → A → A    := has_div.div
-def dvd     {A : Type u} [has_dvd A]     : A → A → Prop := has_dvd.dvd
-def mod     {A : Type u} [has_mod A]     : A → A → A    := has_mod.mod
-def neg     {A : Type u} [has_neg A]     : A → A        := has_neg.neg
-def inv     {A : Type u} [has_inv A]     : A → A        := has_inv.inv
-def le      {A : Type u} [has_le A]      : A → A → Prop := has_le.le
-def lt      {A : Type u} [has_lt A]      : A → A → Prop := has_lt.lt
-def append  {A : Type u} [has_append A]  : A → A → A    := has_append.append
-def andthen {A : Type u} [has_andthen A] : A → A → A    := has_andthen.andthen
-
-@[reducible] def ge {A : Type u} [s : has_le A] (a b : A) : Prop := le b a
-@[reducible] def gt {A : Type u} [s : has_lt A] (a b : A) : Prop := lt b a
+def zero     {A : Type u} [has_zero A]     : A            := has_zero.zero A
+def one      {A : Type u} [has_one A]      : A            := has_one.one A
+def add      {A : Type u} [has_add A]      : A → A → A    := has_add.add
+def mul      {A : Type u} [has_mul A]      : A → A → A    := has_mul.mul
+def sub      {A : Type u} [has_sub A]      : A → A → A    := has_sub.sub
+def div      {A : Type u} [has_div A]      : A → A → A    := has_div.div
+def dvd      {A : Type u} [has_dvd A]      : A → A → Prop := has_dvd.dvd
+def mod      {A : Type u} [has_mod A]      : A → A → A    := has_mod.mod
+def neg      {A : Type u} [has_neg A]      : A → A        := has_neg.neg
+def inv      {A : Type u} [has_inv A]      : A → A        := has_inv.inv
+def le       {A : Type u} [has_le A]       : A → A → Prop := has_le.le
+def lt       {A : Type u} [has_lt A]       : A → A → Prop := has_lt.lt
+def append   {A : Type u} [has_append A]   : A → A → A    := has_append.append
+def andthen  {A : Type u} [has_andthen A]  : A → A → A    := has_andthen.andthen
+def union    {A : Type u} [has_union A]    : A → A → A    := has_union.union
+def inter    {A : Type u} [has_inter A]    : A → A → A    := has_inter.inter
+def sdiff    {A : Type u} [has_sdiff A]    : A → A → A    := has_sdiff.sdiff
+def subset   {A : Type u} [has_subset A]   : A → A → Prop := has_subset.subset
+def ssubset  {A : Type u} [has_ssubset A]  : A → A → Prop := has_ssubset.ssubset
+@[reducible]
+def ge {A : Type u} [has_le A] (a b : A) : Prop := le b a
+@[reducible]
+def gt {A : Type u} [has_lt A] (a b : A) : Prop := lt b a
+@[reducible]
+def superset {A : Type u} [has_subset A] (a b : A) : Prop := subset b a
+@[reducible]
+def ssuperset {A : Type u} [has_ssubset A] (a b : A) : Prop := ssubset b a
 def bit0 {A : Type u} [s  : has_add A] (a  : A)                 : A := add a a
 def bit1 {A : Type u} [s₁ : has_one A] [s₂ : has_add A] (a : A) : A := add (bit0 a) one
 
 attribute [pattern] zero one bit0 bit1 add
 
+def insert {A : Type u} {C : Type u → Type v} [insertable A C] : A → C A → C A :=
+insertable.insert
+
+/- The empty collection -/
+def empty_col {A : Type u} {C : Type u → Type v} [insertable A C] : C A :=
+insertable.empty A C
+
+def singleton {A : Type u} {C : Type u → Type v} [insertable A C] (a : A) : C A :=
+insert a empty_col
+
+def sep {A : Type u} {C : Type u → Type v} [separable A C] : (A → Prop) → C A → C A :=
+separable.sep
+
+def mem {A : Type u} {C : Type u → Type v} [has_mem A C] : A → C A → Prop :=
+has_mem.mem
+
+/- num, pos_num instances -/
+
 instance : has_zero num :=
 ⟨num.zero⟩
 
@@ -195,6 +323,8 @@ instance : has_add num :=
 def std.priority.default : num := 1000
 def std.priority.max     : num := 4294967295
 
+/- nat basic instances -/
+
 namespace nat
   protected def prio := num.add std.priority.default 100
 
@@ -234,92 +364,37 @@ def std.prec.max_plus :=
 num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ
   (num.succ std.prec.max)))))))))
 
-/- Logical operations and relations -/
-
-reserve prefix `¬`:40
-reserve prefix `~`:40
-reserve infixr ` ∧ `:35
-reserve infixr ` /\ `:35
-reserve infixr ` \/ `:30
-reserve infixr ` ∨ `:30
-reserve infix ` <-> `:20
-reserve infix ` ↔ `:20
-reserve infix ` = `:50
-reserve infix ` ≠ `:50
-reserve infix ` ≈ `:50
-reserve infix ` ~ `:50
-reserve infix ` ≡ `:50
-reserve infixl ` ⬝ `:75
-reserve infixr ` ▸ `:75
-reserve infixr ` ▹ `:75
-
-/- types and type constructors -/
-
-reserve infixr ` ⊕ `:30
-reserve infixr ` × `:35
-
-/- arithmetic operations -/
-
-reserve infixl ` + `:65
-reserve infixl ` - `:65
-reserve infixl ` * `:70
-reserve infixl ` / `:70
-reserve infixl ` % `:70
-reserve prefix `-`:100
-reserve infix ` ^ `:80
-
-reserve infixr ` ∘ `:90                 -- input with \comp
 reserve postfix `⁻¹`:std.prec.max_plus  -- input with \sy or \-1 or \inv
 
-reserve infix ` <= `:50
-reserve infix ` ≤ `:50
-reserve infix ` < `:50
-reserve infix ` >= `:50
-reserve infix ` ≥ `:50
-reserve infix ` > `:50
-
-/- boolean operations -/
-
-reserve infixl ` && `:70
-reserve infixl ` || `:65
-
-/- set operations -/
-
-reserve infix ` ∈ `:50
-reserve infix ` ∉ `:50
-reserve infixl ` ∩ `:70
-reserve infixl ` ∪ `:65
-reserve infix ` ⊆ `:50
-reserve infix ` ⊇ `:50
-reserve infix ` ' `:75   -- for the image of a set under a function
-reserve infix ` '- `:75  -- for the preimage of a set under a function
-
-/- other symbols -/
-
-reserve infix ` ∣ `:50
-reserve infixl ` ++ `:65
-reserve infixr ` :: `:67
-reserve infixl `; `:1
-
-infix +    := add
-infix *    := mul
-infix -    := sub
-infix /    := div
-infix ∣    := dvd
-infix %    := mod
-prefix -   := neg
-postfix ⁻¹ := inv
-infix <=   := le
-infix >=   := ge
-infix ≤    := le
-infix ≥    := ge
-infix <    := lt
-infix >    := gt
-infix ++   := append
-infix ;    := andthen
+infix =        := eq
+infix ∈        := mem
+notation a ∉ s := ¬ mem a s
+infix +        := add
+infix *        := mul
+infix -        := sub
+infix /        := div
+infix ∣        := dvd
+infix %        := mod
+prefix -       := neg
+postfix ⁻¹     := inv
+infix <=       := le
+infix >=       := ge
+infix ≤        := le
+infix ≥        := ge
+infix <        := lt
+infix >        := gt
+infix ++       := append
+infix ;        := andthen
+notation `∅`   := empty_col
+infix ∪        := union
+infix ∩        := inter
+infix ⊆        := subset
+infix ⊇        := superset
+infix ⊂        := ssubset
+infix ⊃        := ssuperset
+infix \        := sdiff
 
 /- eq basic support -/
-notation a = b := eq a b
 
 @[pattern] def rfl {A : Type u} {a : A} : a = a := eq.refl a
 
diff --git a/library/init/default.lean b/library/init/default.lean
index 34ce6de7f6..c388186d56 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.datatypes init.logic
+import init.core init.logic
 import init.relation init.nat init.prod init.sum init.combinator
 import init.bool init.unit init.num init.sigma init.setoid init.quot
 import init.funext init.function init.subtype init.classical
diff --git a/library/init/list.lean b/library/init/list.lean
index 5c177c444e..8c145dbfd1 100644
--- a/library/init/list.lean
+++ b/library/init/list.lean
@@ -18,12 +18,52 @@ instance (A : Type u) : inhabited (list A) :=
 variables {A : Type u} {B : Type v}
 
 namespace list
-def append : list A → list A → list A
+protected def append : list A → list A → list A
 | []       l := l
 | (h :: s) t := h :: (append s t)
 
 instance : has_append (list A) :=
-⟨append⟩
+⟨list.append⟩
+
+protected def mem : A → list A → Prop
+| a []       := false
+| a (b :: l) := a = b ∨ mem a l
+
+instance : has_mem A list :=
+⟨list.mem⟩
+
+instance decidable_mem [decidable_eq A] (a : A) : ∀ (l : list A), decidable (a ∈ l)
+| []     := is_false not_false
+| (b::l) :=
+  if h₁ : a = b then is_true (or.inl h₁)
+  else match decidable_mem l with
+  | is_true  h₂ := is_true (or.inr h₂)
+  | is_false h₂ := is_false (not_or h₁ h₂)
+  end
+
+def concat : list A → A → list A
+| []     a := [a]
+| (b::l) a := b :: concat l a
+
+protected def insert [decidable_eq A] (a : A) (l : list A) : list A :=
+if a ∈ l then l else concat l a
+
+instance [decidable_eq A] : insertable A list :=
+⟨list.nil, list.insert⟩
+
+protected def union [decidable_eq A] : list A → list A → list A
+| l₁ []      := l₁
+| l₁ (a::l₂) := union (insert a l₁) l₂
+
+instance [decidable_eq A] : has_union (list A) :=
+⟨list.union⟩
+
+protected def inter [decidable_eq A] : list A → list A → list A
+| []      l₂ := []
+| (a::l₁) l₂ := if a ∈ l₂ then a :: inter l₁ l₂ else inter l₁ l₂
+
+instance [decidable_eq A] : has_inter (list A) :=
+⟨list.inter⟩
 
 def length : list A → nat
 | []       := 0
@@ -44,13 +84,9 @@ def tail : list A → list A
 | []       := []
 | (a :: l) := l
 
-def concat : Π (x : A), list A → list A
-| a []       := [a]
-| a (b :: l) := b :: concat a l
-
 def reverse : list A → list A
 | []       := []
-| (a :: l) := concat a (reverse l)
+| (a :: l) := concat (reverse l) a
 
 def map (f : A → B) : list A → list B
 | []       := []
diff --git a/library/init/list_classes.lean b/library/init/list_classes.lean
index 5b42bb493d..47517ef63b 100644
--- a/library/init/list_classes.lean
+++ b/library/init/list_classes.lean
@@ -9,17 +9,14 @@ open list
 
 universe variables u v
 
-@[inline] def list_fmap {A : Type u} {B : Type v} (f : A → B) (l : list A) : list B :=
-map f l
-
-@[inline] def list_bind {A : Type u} {B : Type v} (a : list A) (b : A → list B) : list B :=
+@[inline] def list.bind {A : Type u} {B : Type v} (a : list A) (b : A → list B) : list B :=
 join (map b a)
 
-@[inline] def list_return {A : Type u} (a : A) : list A :=
+@[inline] def list.ret {A : Type u} (a : A) : list A :=
 [a]
 
 instance : monad list :=
-⟨@list_fmap, @list_return, @list_bind⟩
+⟨@map, @list.ret, @list.bind⟩
 
 instance : alternative list :=
-⟨@list_fmap, @list_return, @fapp _ _, @nil, @list.append⟩
+⟨@map, @list.ret, @fapp _ _, @nil, @list.append⟩
diff --git a/library/init/logic.lean b/library/init/logic.lean
index db4ddd3c61..3771f08d95 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 -/
 prelude
-import init.datatypes
+import init.core
 
 universe variables u v w
 
@@ -22,9 +22,6 @@ assume hp, h₂ (h₁ hp)
 
 def trivial : true := ⟨⟩
 
-def not (a : Prop) := a → false
-prefix `¬` := not
-
 @[inline] def absurd {a : Prop} {b : Type v} (h₁ : a) (h₂ : ¬a) : b :=
 false.rec b (h₂ h₁)
 
@@ -509,6 +506,10 @@ attribute [simp]
 lemma or_self (a : Prop) : a ∨ a ↔ a :=
 iff.intro (or.rec id id) or.inl
 
+lemma not_or {a b : Prop} : ¬ a → ¬ b → ¬ (a ∨ b)
+| hna hnb (or.inl ha) := absurd ha hna
+| hna hnb (or.inr hb) := absurd hb hnb
+
 /- or resolution rulse -/
 
 def or.resolve_left {a b : Prop} (h : a ∨ b) (na : ¬ a) : b :=
@@ -616,11 +617,10 @@ exists_congr (λ x, and_congr (h x) (forall_congr (λ y, imp_congr (h y) iff.rfl
 
 /- decidable -/
 
-class inductive decidable (p : Prop)
-| is_false : ¬p → decidable
-| is_true :  p → decidable
+def decidable.to_bool (p : Prop) [h : decidable p] : bool :=
+decidable.cases_on h (λ h₁, bool.ff) (λ h₂, bool.tt)
 
-export decidable (is_true is_false)
+export decidable (is_true is_false to_bool)
 
 instance decidable.true : decidable true :=
 is_true trivial
@@ -655,9 +655,6 @@ namespace decidable
 
   lemma by_contradiction [decidable p] (h : ¬p → false) : p :=
   if h₁ : p then h₁ else false.rec _ (h h₁)
-
-  def to_bool (p : Prop) [h : decidable p] : bool :=
-  decidable.cases_on h (λ h₁, bool.ff) (λ h₂, bool.tt)
 end decidable
 
 section
@@ -703,10 +700,6 @@ section
   and.decidable
 end
 
-@[reducible] def decidable_pred {A : Type u} (r : A → Prop) := Π (a : A), decidable (r a)
-@[reducible] def decidable_rel  {A : Type u} (r : A → A → Prop) := Π (a b : A), decidable (r a b)
-@[reducible] def decidable_eq   (A : Type u) := decidable_rel (@eq A)
-
 instance {A : Type u} [decidable_eq A] (a b : A) : decidable (a ≠ b) :=
 implies.decidable
 
diff --git a/library/init/set.lean b/library/init/set.lean
index b88017d29f..7153dd9748 100644
--- a/library/init/set.lean
+++ b/library/init/set.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.logic init.collection
+import init.logic init.functor
 
 universe variables u v
 
@@ -16,19 +16,17 @@ p
 namespace set
 variables {A : Type u} {B : Type v}
 
-def mem (a : A) (s : set A) :=
+protected def mem (a : A) (s : set A) :=
 s a
 
-infix ∈ := mem
-notation a ∉ s := ¬ mem a s
+instance : has_mem A set :=
+⟨set.mem⟩
 
-def subset (s₁ s₂ : set A) : Prop :=
-∀ ⦃a⦄, a ∈ s₁ → a ∈ s₂
-infix ⊆ := subset
+protected def subset (s₁ s₂ : set A) :=
+∀ a, a ∈ s₁ → a ∈ s₂
 
-def superset (s₁ s₂ : set A) : Prop :=
-s₂ ⊆ s₁
-infix ⊇ := superset
+instance : has_subset (set A) :=
+⟨set.subset⟩
 
 private def sep (p : A → Prop) (s : set A) : set A :=
 {a | a ∈ s ∧ p a}
@@ -45,13 +43,17 @@ private def insert (a : A) (s : set A) : set A :=
 instance : insertable A set :=
 ⟨empty, insert⟩
 
-def union (s₁ s₂ : set A) : set A :=
+protected def union (s₁ s₂ : set A) : set A :=
 {a | a ∈ s₁ ∨ a ∈ s₂}
-notation s₁ ∪ s₂ := union s₁ s₂
 
-def inter (s₁ s₂ : set A) : set A :=
+instance : has_union (set A) :=
+⟨set.union⟩
+
+protected def inter (s₁ s₂ : set A) : set A :=
 {a | a ∈ s₁ ∧ a ∈ s₂}
-notation s₁ ∩ s₂ := inter s₁ s₂
+
+instance : has_inter (set A) :=
+⟨set.inter⟩
 
 def compl (s : set A) : set A :=
 {a | a ∉ s}
@@ -59,9 +61,11 @@ def compl (s : set A) : set A :=
 instance : has_neg (set A) :=
 ⟨compl⟩
 
-def diff (s t : set A) : set A :=
+protected def diff (s t : set A) : set A :=
 {a ∈ s | a ∉ t}
-infix `\`:70 := diff
+
+instance : has_sdiff (set A) :=
+⟨set.diff⟩
 
 def powerset (s : set A) : set (set A) :=
 {t | t ⊆ s}
@@ -69,5 +73,8 @@ prefix `𝒫`:100 := powerset
 
 def image (f : A → B) (s : set A) : set B :=
 {b | ∃ a, a ∈ s ∧ f a = b}
-infix ` ' ` := image
+
+instance : functor set :=
+⟨@set.image⟩
+
 end set
diff --git a/library/init/sigma.lean b/library/init/sigma.lean
index fdf24a3ab4..325fc66bd8 100644
--- a/library/init/sigma.lean
+++ b/library/init/sigma.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 -/
 prelude
-import init.datatypes init.num init.wf init.logic
+import init.logic init.num init.wf
 
 definition dpair := @sigma.mk
 notation `Σ` binders `, ` r:(scoped P, sigma P) := r
diff --git a/library/init/subtype.lean b/library/init/subtype.lean
index ac27f43f55..98923bd255 100644
--- a/library/init/subtype.lean
+++ b/library/init/subtype.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura, Jeremy Avigad
 -/
 prelude
-import init.datatypes init.logic
+import init.logic
 open decidable
 
 universe variables u
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 3d3459438e..0847125082 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -82,7 +82,7 @@ void init_token_table(token_table & t) {
          {"have", 0}, {"suppose", 0}, {"show", 0}, {"suffices", 0}, {"obtain", 0},
          {"do", 0}, {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"hiding", 0}, {"replacing", 0}, {"renaming", 0},
          {"from", 0}, {"(", g_max_prec}, {"`(", g_max_prec}, {"`", g_max_prec},
-         {"%%", g_max_prec}, {"()", g_max_prec}, {")", 0},
+         {"%%", g_max_prec}, {"()", g_max_prec}, {")", 0}, {"'", 0},
          {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type*", g_max_prec},
          {"{|", g_max_prec}, {"|}", 0}, {"(:", g_max_prec}, {":)", 0},
diff --git a/tests/lean/run/list_notation.lean b/tests/lean/run/list_notation.lean
new file mode 100644
index 0000000000..53994023f7
--- /dev/null
+++ b/tests/lean/run/list_notation.lean
@@ -0,0 +1,27 @@
+open nat
+
+vm_eval [1, 2, 3]
+
+vm_eval to_bool $ 1 ∈ [1, 2, 3]
+
+vm_eval to_bool $ 4 ∈ [1, 2, 3]
+
+vm_eval [1, 2, 3] ++ [3, 4]
+
+vm_eval 2 :: [3, 4]
+
+vm_eval ([] : list nat)
+
+vm_eval (∅ : list nat)
+
+vm_eval ({1, 3, 2, 2, 3, 1} : list nat)
+
+vm_eval [1, 2, 3] ∪ [3, 4, 1, 5]
+
+vm_eval [1, 2, 3] ∩ [3, 4, 1, 5]
+
+vm_eval (mul 10) <$> [1, 2, 3]
+
+check ({1, 2, 3} : list nat)
+
+check ({1, 2, 3, 4} : set nat)
diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out
index fd7d6c5536..c639c7405e 100644
--- a/tests/lean/struct_class.lean.expected.out
+++ b/tests/lean/struct_class.lean.expected.out
@@ -1,7 +1,6 @@
 alternative : (Type u → Type v) → Type (max (u+1) v)
 applicative : (Type u → Type v) → Type (max (u+1) v)
 decidable : Prop → Type
-decidable_separable : Type u → (Type u → Type v) → Type (max 1 (imax (max 1 u) (max 1 u) v))
 functor : (Type u → Type v) → Type (max (u+1) v)
 has_add : Type u → Type (max 1 u)
 has_andthen : Type u → Type (max 1 u)
@@ -12,22 +11,28 @@ has_coe_to_fun : Type u → Type (max u (v+1))
 has_coe_to_sort : Type u → Type (max u (v+1))
 has_div : Type u → Type (max 1 u)
 has_dvd : Type u → Type (max 1 u)
+has_inter : Type u → Type (max 1 u)
 has_inv : Type u → Type (max 1 u)
 has_le : Type u → Type (max 1 u)
 has_lift : Type u → Type v → Type (max 1 (imax u v))
 has_lift_t : Type u → Type v → Type (max 1 (imax u v))
 has_lt : Type u → Type (max 1 u)
+has_mem : Type u → (Type u → Type v) → Type (max 1 u v)
 has_mod : Type u → Type (max 1 u)
 has_mul : Type u → Type (max 1 u)
 has_neg : Type u → Type (max 1 u)
 has_one : Type u → Type (max 1 u)
 has_ordering : Type → Type
+has_sdiff : Type u → Type (max 1 u)
 has_sizeof : Type u → Type (max 1 u)
+has_ssubset : Type u → Type (max 1 u)
 has_sub : Type u → Type (max 1 u)
+has_subset : Type u → Type (max 1 u)
 has_to_format : Type u → Type (max 1 u)
 has_to_pexpr : Type u → Type (max 1 u)
 has_to_string : Type u → Type (max 1 u)
 has_to_tactic_format : Type → Type
+has_union : Type u → Type (max 1 u)
 has_zero : Type u → Type (max 1 u)
 inhabited : Type u → Type (max 1 u)
 insertable : Type u → (Type u → Type v) → Type (max 1 (imax u v) v)
@@ -41,7 +46,6 @@ subsingleton : Type u → Prop
 alternative : (Type u → Type v) → Type (max (u+1) v)
 applicative : (Type u → Type v) → Type (max (u+1) v)
 decidable : Prop → Type
-decidable_separable : Type u → (Type u → Type v) → Type (max 1 (imax (max 1 u) (max 1 u) v))
 functor : (Type u → Type v) → Type (max (u+1) v)
 has_add : Type u → Type (max 1 u)
 has_andthen : Type u → Type (max 1 u)
@@ -52,22 +56,28 @@ has_coe_to_fun : Type u → Type (max u (v+1))
 has_coe_to_sort : Type u → Type (max u (v+1))
 has_div : Type u → Type (max 1 u)
 has_dvd : Type u → Type (max 1 u)
+has_inter : Type u → Type (max 1 u)
 has_inv : Type u → Type (max 1 u)
 has_le : Type u → Type (max 1 u)
 has_lift : Type u → Type v → Type (max 1 (imax u v))
 has_lift_t : Type u → Type v → Type (max 1 (imax u v))
 has_lt : Type u → Type (max 1 u)
+has_mem : Type u → (Type u → Type v) → Type (max 1 u v)
 has_mod : Type u → Type (max 1 u)
 has_mul : Type u → Type (max 1 u)
 has_neg : Type u → Type (max 1 u)
 has_one : Type u → Type (max 1 u)
 has_ordering : Type → Type
+has_sdiff : Type u → Type (max 1 u)
 has_sizeof : Type u → Type (max 1 u)
+has_ssubset : Type u → Type (max 1 u)
 has_sub : Type u → Type (max 1 u)
+has_subset : Type u → Type (max 1 u)
 has_to_format : Type u → Type (max 1 u)
 has_to_pexpr : Type u → Type (max 1 u)
 has_to_string : Type u → Type (max 1 u)
 has_to_tactic_format : Type → Type
+has_union : Type u → Type (max 1 u)
 has_zero : Type u → Type (max 1 u)
 inhabited : Type u → Type (max 1 u)
 insertable : Type u → (Type u → Type v) → Type (max 1 (imax u v) v)