max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(init/algebra/group): parameterize transport_mul_to_add

Browse source
This commit is contained in:
Mario Carneiro 2017-07-21 23:15:20 +01:00 • committed by Gabriel Ebner
parent bd19736b21
commit 9ca2113790
1 changed files with 11 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
library/init/algebra/group.lean
View file

@ -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⟩