Commit 2020-05-27 07:09 0d6d0b0f

chore(*): split long lines, unindent in namespaces (#2834) The diff is large but here is the word diff (search for [- or [+):

$ git diff --word-diff=plain --ignore-all-space master | grep '(^---|\[-|\[\+)'
--- a/src/algebra/big_operators.lean
[-λ l, @is_group_anti_hom.map_prod _ _ _ _ _ inv_is_group_anti_hom l-]-- TODO there is probably a cleaner proof of this
        { have : [-(to_finset s).sum (λx,-]{+∑ x in s.to_finset,+} ite (x = a) 1 [-0)-]{+0+} = [-({a} : finset α).sum (λx,-]{+∑ x in {a},+} ite (x = a) 1 [-0),-]
[-          { apply (finset.sum_subset _ _).symm,-]{+0,+}
          { [-intros _ H, rwa mem_singleton.1 H },-]
[-            { exact λ _ _ H, if_neg (mt finset.mem_singleton.2 H) }-]{+rw [finset.sum_ite_eq', if_pos h, finset.sum_singleton, if_pos rfl],+} },
--- a/src/algebra/category/Group/basic.lean
[-a-]{+an+} `add_equiv` between `add_group`s."]
--- a/src/algebra/category/Group/colimits.lean
--- a/src/algebra/category/Mon/basic.lean
[-a-]{+an+} `add_equiv` between `add_monoid`s."]
[-a-]{+an+} `add_equiv` between `add_comm_monoid`s."]
--- a/src/algebra/free.lean
--- a/src/algebra/group/units.lean
--- a/src/algebra/group/units_hom.lean
--- a/src/category_theory/category/default.lean
[-universes v u-]-- The order in this declaration matters: v often needs to be explicitly specified while u often
--- a/src/control/monad/cont.lean
    simp [-[call_cc,except_t.call_cc,call_cc_bind_right,except_t.goto_mk_label,map_eq_bind_pure_comp,bind_assoc,@call_cc_bind_left-]{+[call_cc,except_t.call_cc,call_cc_bind_right,except_t.goto_mk_label,map_eq_bind_pure_comp,+}
  call_cc_bind_left  := by { intros, simp [-[call_cc,option_t.call_cc,call_cc_bind_right,option_t.goto_mk_label,map_eq_bind_pure_comp,bind_assoc,@call_cc_bind_left-]{+[call_cc,option_t.call_cc,call_cc_bind_right,+}
  call_cc_bind_left  := by { intros, simp [-[call_cc,state_t.call_cc,call_cc_bind_left,(>>=),state_t.bind,state_t.goto_mk_label],-]{+[call_cc,state_t.call_cc,call_cc_bind_left,(>>=),+}
  call_cc_dummy := by { intros, simp [-[call_cc,state_t.call_cc,call_cc_bind_right,(>>=),state_t.bind,@call_cc_dummy-]{+[call_cc,state_t.call_cc,call_cc_bind_right,(>>=),+}
  call_cc_bind_left  := by { intros, simp [-[call_cc,reader_t.call_cc,call_cc_bind_left,reader_t.goto_mk_label],-]{+[call_cc,reader_t.call_cc,call_cc_bind_left,+}
--- a/src/control/monad/writer.lean
--- a/src/control/traversable/basic.lean
   online at <http://arxiv.org/pdf/1202.2919>[-Synopsis-]
--- a/src/data/analysis/filter.lean
--- a/src/data/equiv/basic.lean
--- a/src/data/fin.lean
--- a/src/data/finset.lean
  [-by-]{+{+} rw [-[eq],-]{+[eq] },+}
--- a/src/data/hash_map.lean
--- a/src/data/int/basic.lean
--- a/src/data/list/basic.lean
--- a/src/data/list/tfae.lean
--- a/src/data/num/lemmas.lean
[-Properties of the binary representation of integers.-]
--- a/src/data/zsqrtd/basic.lean
--- a/src/group_theory/congruence.lean
with [-a-]{+an+} addition."]
@[to_additive Sup_eq_add_con_gen "The supremum of a set of additive congruence relations [-S-]{+`S`+} equals
--- a/src/group_theory/monoid_localization.lean
--- a/src/group_theory/submonoid.lean
--- a/src/number_theory/dioph.lean
--- a/src/set_theory/ordinal.lean
--- a/src/tactic/apply.lean
--- a/src/tactic/lean_core_docs.lean
--- a/src/tactic/lint/type_classes.lean
--- a/src/tactic/omega/main.lean
--- a/test/coinductive.lean
--- a/test/localized/import3.lean
--- a/test/norm_num.lean
--- a/test/tidy.lean
--- a/test/where.lean

P.S.: I don't know how to make git diff hide all non-interesting chunks.