From f176c272b46daf1e043bf33c53e10d882ec9f18d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Jan 2017 18:43:05 -0800
Subject: [PATCH] refactor(library/init/core): simpler has_mem type class with
 out_param

---
 library/data/stream.lean           |  2 +-
 library/init/core.lean             |  4 ++--
 library/init/data/list/basic.lean  |  2 +-
 library/init/data/list/lemmas.lean |  4 ++--
 library/init/data/set.lean         |  2 +-
 tests/lean/run/regset.lean         | 13 +++++++++++++
 6 files changed, 20 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/run/regset.lean

diff --git a/library/data/stream.lean b/library/data/stream.lean
index d2fac509c7..e1fc1ae6bc 100644
--- a/library/data/stream.lean
+++ b/library/data/stream.lean
@@ -77,7 +77,7 @@ rfl
 
 protected def mem (a : α) (s : stream α) := any (λ b, a = b) s
 
-instance : has_mem α stream :=
+instance : has_mem α (stream α) :=
 ⟨stream.mem⟩
 
 lemma mem_cons (a : α) (s : stream α) : a ∈ (a::s) :=
diff --git a/library/init/core.lean b/library/init/core.lean
index db4520628f..7003244496 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -257,7 +257,7 @@ class has_insert   (α : Type u) (γ : Type u → Type v) := (insert : α → γ
 class has_sep (α : Type u) (γ : Type u → Type v) :=
 (sep : (α → Prop) → γ α → γ α)
 /- Type class for set-like membership -/
-class has_mem (α : Type u) (γ : Type u → Type v) := (mem : α → γ α → Prop)
+class has_mem (α : out_param (Type u)) (γ : Type v) := (mem : α → γ → Prop)
 
 def zero     {α : Type u} [has_zero α]     : α            := has_zero.zero α
 def one      {α : Type u} [has_one α]      : α            := has_one.one α
@@ -304,7 +304,7 @@ insert a emptyc
 def sep {α : Type u} {γ : Type u → Type v} [has_sep α γ] : (α → Prop) → γ α → γ α :=
 has_sep.sep
 
-def mem {α : Type u} {γ : Type u → Type v} [has_mem α γ] : α → γ α → Prop :=
+def mem {α : Type u} {γ : Type v} [has_mem α γ] : α → γ → Prop :=
 has_mem.mem
 
 /- num, pos_num instances -/
diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean
index 5fdb26c929..d722e0294a 100644
--- a/library/init/data/list/basic.lean
+++ b/library/init/data/list/basic.lean
@@ -29,7 +29,7 @@ protected def mem : α → list α → Prop
 | a []       := false
 | a (b :: l) := a = b ∨ mem a l
 
-instance : has_mem α list :=
+instance : has_mem α (list α) :=
 ⟨list.mem⟩
 
 instance decidable_mem [decidable_eq α] (a : α) : ∀ (l : list α), decidable (a ∈ l)
diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean
index 25d3745522..f07d4a9c43 100644
--- a/library/init/data/list/lemmas.lean
+++ b/library/init/data/list/lemmas.lean
@@ -43,10 +43,10 @@ rfl
 
 /- list membership -/
 @[simp]
-lemma mem_nil_iff (a : α) : a ∈ [] ↔ false :=
+lemma mem_nil_iff (a : α) : a ∈ ([] : list α) ↔ false :=
 iff.rfl
 
-@[simp] lemma not_mem_nil (a : α) : a ∉ [] :=
+@[simp] lemma not_mem_nil (a : α) : a ∉ ([] : list α) :=
 iff.mp $ mem_nil_iff a
 
 @[simp] lemma mem_cons_self (a : α) (l : list α) : a ∈ a :: l :=
diff --git a/library/init/data/set.lean b/library/init/data/set.lean
index 93f6d7acf9..cfadbf276c 100644
--- a/library/init/data/set.lean
+++ b/library/init/data/set.lean
@@ -18,7 +18,7 @@ variables {α : Type u} {β : Type v}
 protected def mem (a : α) (s : set α) :=
 s a
 
-instance : has_mem α set :=
+instance : has_mem α (set α) :=
 ⟨set.mem⟩
 
 protected def subset (s₁ s₂ : set α) :=
diff --git a/tests/lean/run/regset.lean b/tests/lean/run/regset.lean
new file mode 100644
index 0000000000..f8938aa8ec
--- /dev/null
+++ b/tests/lean/run/regset.lean
@@ -0,0 +1,13 @@
+namespace regset
+
+section
+parameter symbol : Type
+
+@[reducible] def lang : Type :=
+set (list symbol)
+
+def concat : lang → lang → lang :=
+λ a b : lang, { ll : list symbol | ∃xs ys : list symbol, ll = list.append xs ys ∧ xs ∈ a ∧ ys ∈ b }
+
+end
+end regset