refactor(library/init/core): simpler has_mem type class with out_param

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) :=

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 -/

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)

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 :=

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 α) :=

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