From bcbe5ec9f4b04832aa215d081fccc07c7a920446 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 9 Mar 2018 16:36:44 +0100
Subject: [PATCH] refactor(init/category/functor): merge `has_map` into
 `functor`

---
 doc/changes.md                     |  1 +
 library/init/category/functor.lean | 12 +++++-------
 library/init/category/lawful.lean  |  4 ++--
 library/init/data/option_t.lean    |  2 +-
 library/init/data/set.lean         |  4 ++--
 library/init/meta/tactic.lean      |  2 +-
 6 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/doc/changes.md b/doc/changes.md
index 49311c65bf..28a37c60d3 100644
--- a/doc/changes.md
+++ b/doc/changes.md
@@ -245,6 +245,7 @@ master branch (aka work in progress branch)
 * `state(_t).{read,write}` ~> `{get,put}` (general operations defined on any `monad_state_lift`)
 * deleted `monad.monad_transformer`
 * deleted `monad.lift{n}`. Use `f <$> a1 <*> ... <*> an` instead of `monad.lift{n} f a1 ... an`.
+* merged `has_map` into `functor`
 
 v3.3.0 (14 September 2017)
 -------------
diff --git a/library/init/category/functor.lean b/library/init/category/functor.lean
index bd1aab30e7..9e41319e3d 100644
--- a/library/init/category/functor.lean
+++ b/library/init/category/functor.lean
@@ -8,15 +8,13 @@ import init.core init.function init.meta.name
 open function
 universes u v
 
-class has_map (f : Type u → Type v) : Type (max (u+1) v) :=
+class functor (f : Type u → Type v) : Type (max (u+1) v) :=
 (map : Π {α β : Type u}, (α → β) → f α → f β)
 (map_const : Π {α β : Type u}, α → f β → f α := λ α β, map ∘ const β)
 
-infixr ` <$> `:100 := has_map.map
-infixr ` <$ `:100  := has_map.map_const
+infixr ` <$> `:100 := functor.map
+infixr ` <$ `:100  := functor.map_const
 
-@[reducible] def has_map.map_const_rev {f : Type u → Type v} [has_map f] {α β : Type u} : f β → α → f α :=
+@[reducible] def functor.map_const_rev {f : Type u → Type v} [functor f] {α β : Type u} : f β → α → f α :=
 λ a b, b <$ a
-infixr ` $> `:100  := has_map.map_const_rev
-
-class functor (f : Type u → Type v) extends has_map f
+infixr ` $> `:100  := functor.map_const_rev
diff --git a/library/init/category/lawful.lean b/library/init/category/lawful.lean
index e75d98523f..a932749f68 100644
--- a/library/init/category/lawful.lean
+++ b/library/init/category/lawful.lean
@@ -14,7 +14,7 @@ open tactic
 meta def control_laws_tac := whnf_target >> intros >> to_expr ``(rfl) >>= exact
 
 class is_lawful_functor (f : Type u → Type v) [functor f] : Prop :=
-(map_const_eq : ∀ {α β : Type u}, @has_map.map_const f _ α β = (<$>) ∘ const β . control_laws_tac)
+(map_const_eq : ∀ {α β : Type u}, ((<$) : α → f β → f α) = (<$>) ∘ const β . control_laws_tac)
 -- `functor` is indeed a categorical functor
 (id_map       : Π {α : Type u} (x : f α), id <$> x = x)
 (comp_map     : Π {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x)
@@ -67,7 +67,7 @@ lemma bind_ext_congr {α β} {m : Type u → Type v} [has_bind m] {x : m α} {f
   x >>= f = x >>= g :=
 λ h, by simp [show f = g, from funext h]
 
-lemma map_ext_congr {α β} {m : Type u → Type v} [has_map m] {x : m α} {f g : α → β} :
+lemma map_ext_congr {α β} {m : Type u → Type v} [functor m] {x : m α} {f g : α → β} :
   (∀ a, f a = g a) →
   (f <$> x : m β) = g <$> x :=
 λ h, by simp [show f = g, from funext h]
diff --git a/library/init/data/option_t.lean b/library/init/data/option_t.lean
index 6757bdb7bf..2ceacb0f6b 100644
--- a/library/init/data/option_t.lean
+++ b/library/init/data/option_t.lean
@@ -30,7 +30,7 @@ instance {m : Type u → Type v} [monad m] : monad (option_t m) :=
 instance {m : Type u → Type v} [monad m] [is_lawful_monad m] : is_lawful_monad (option_t m) :=
 { id_map := begin
     intros,
-    simp [has_map.map, option_t_bind, function.comp],
+    simp [(<$>), option_t_bind, function.comp],
     have h : option_t_bind._match_1 option_t_return = @pure m _ (option α),
     { funext s, cases s; refl },
     { simp [h, bind_pure] },
diff --git a/library/init/data/set.lean b/library/init/data/set.lean
index 97916db83d..af3a7d5dc3 100644
--- a/library/init/data/set.lean
+++ b/library/init/data/set.lean
@@ -87,13 +87,13 @@ instance : functor set :=
 instance : is_lawful_functor set :=
 { id_map := begin
     intros _ s, funext b,
-    dsimp [has_map.map, image, set_of],
+    dsimp [image, set_of],
     exact propext ⟨λ ⟨b', ⟨_, _⟩⟩, ‹b' = b› ▸ ‹s b'›,
                    λ _, ⟨b, ⟨‹s b›, rfl⟩⟩⟩,
   end,
   comp_map := begin
     intros, funext c,
-    dsimp [has_map.map, image, set_of, function.comp],
+    dsimp [image, set_of, function.comp],
     exact propext ⟨λ ⟨a, ⟨h₁, h₂⟩⟩, ⟨g a, ⟨⟨a, ⟨h₁, rfl⟩⟩, h₂⟩⟩,
                    λ ⟨b, ⟨⟨a, ⟨h₁, h₂⟩⟩, h₃⟩⟩, ⟨a, ⟨h₁, h₂.symm ▸ h₃⟩⟩⟩
   end }
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 2283b1337b..48b0819050 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -192,7 +192,7 @@ has_to_tactic_format.to_tactic_format
 open tactic format
 
 meta instance {α : Type u} [has_to_tactic_format α] : has_to_tactic_format (list α) :=
-⟨has_map.map to_fmt ∘ monad.mapm pp⟩
+⟨λ l, to_fmt <$> l.mmap pp⟩
 
 meta instance (α : Type u) (β : Type v) [has_to_tactic_format α] [has_to_tactic_format β] :
  has_to_tactic_format (α × β) :=