From 9ca2113790f41e34b850cd310d1b8db8f2ea5f2f Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Fri, 21 Jul 2017 23:15:20 +0100
Subject: [PATCH] refactor(init/algebra/group): parameterize
 transport_mul_to_add

---
 library/init/algebra/group.lean | 24 +++++++++++-------------
 1 file changed, 11 insertions(+), 13 deletions(-)

diff --git a/library/init/algebra/group.lean b/library/init/algebra/group.lean
index 818bcac476..9c79b53574 100644
--- a/library/init/algebra/group.lean
+++ b/library/init/algebra/group.lean
@@ -211,7 +211,17 @@ copy_decl_using dict src tgt
 >> copy_attribute `simp src tt tgt
 >> copy_attribute `instance src tt tgt
 
-meta def multiplicative_to_additive_pairs : list (name × name) :=
+/- Transport multiplicative to additive -/
+meta def transport_multiplicative_to_additive (ls : list (name × name)) : command :=
+let dict := rb_map.of_list ls in
+ls.foldl (λ t ⟨src, tgt⟩, do
+  env ← get_env,
+  if (env.get tgt).to_bool = ff
+  then t >> transport_with_dict dict src tgt
+  else t)
+skip
+
+run_cmd transport_multiplicative_to_additive
   [/- map operations -/
    (`has_mul.mul, `has_add.add), (`has_one.one, `has_zero.zero), (`has_inv.inv, `has_neg.neg),
    (`has_mul, `has_add), (`has_one, `has_zero), (`has_inv, `has_neg),
@@ -290,18 +300,6 @@ meta def multiplicative_to_additive_pairs : list (name × name) :=
    (`one_inv, `neg_zero)
 ]
 
-/- Transport multiplicative to additive -/
-meta def transport_multiplicative_to_additive : command :=
-let dict := rb_map.of_list multiplicative_to_additive_pairs in
-multiplicative_to_additive_pairs.foldl (λ t ⟨src, tgt⟩, do
-  env ← get_env,
-  if (env.get tgt).to_bool = ff
-  then t >> transport_with_dict dict src tgt
-  else t)
-skip
-
-run_cmd transport_multiplicative_to_additive
-
 instance add_semigroup_to_is_eq_associative [add_semigroup α] : is_associative α (+) :=
 ⟨add_assoc⟩