Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#14239)
Browse files Browse the repository at this point in the history
I am happy to remove some nolints for you!
  • Loading branch information
leanprover-community-bot committed May 19, 2022
1 parent 83285b2 commit 923a14d
Show file tree
Hide file tree
Showing 2 changed files with 0 additions and 28 deletions.
26 changes: 0 additions & 26 deletions scripts/nolints.txt
Expand Up @@ -389,32 +389,6 @@ apply_nolint stream.unfolds doc_blame
-- data/stream/init.lean
apply_nolint stream.is_bisimulation doc_blame

-- deprecated/group.lean
apply_nolint is_group_hom.comp to_additive_doc
apply_nolint is_group_hom.id to_additive_doc
apply_nolint is_group_hom.injective_iff to_additive_doc
apply_nolint is_group_hom.inv to_additive_doc
apply_nolint is_group_hom.map_inv to_additive_doc
apply_nolint is_group_hom.map_one to_additive_doc
apply_nolint is_group_hom.mk' to_additive_doc
apply_nolint is_group_hom.mul to_additive_doc
apply_nolint is_group_hom.to_is_monoid_hom to_additive_doc
apply_nolint is_monoid_hom.comp to_additive_doc
apply_nolint is_monoid_hom.id to_additive_doc
apply_nolint is_monoid_hom.inv to_additive_doc
apply_nolint is_monoid_hom.map_mul to_additive_doc
apply_nolint is_mul_hom.inv to_additive_doc
apply_nolint is_mul_hom.mul to_additive_doc
apply_nolint is_mul_hom.to_is_monoid_hom to_additive_doc
apply_nolint mul_equiv.is_monoid_hom to_additive_doc
apply_nolint mul_equiv.is_mul_hom to_additive_doc

-- deprecated/subfield.lean
apply_nolint is_subfield doc_blame

-- deprecated/subring.lean
apply_nolint ring.closure doc_blame

-- group_theory/coset.lean
apply_nolint subgroup.card_subgroup_dvd_card to_additive_doc

Expand Down
2 changes: 0 additions & 2 deletions scripts/style-exceptions.txt
Expand Up @@ -27,8 +27,6 @@ src/data/seq/computation.lean : line 12 : ERR_MOD : Module docstring missing, or
src/data/seq/parallel.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/data/seq/seq.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/seq/wseq.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/deprecated/subfield.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/deprecated/subring.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/logic/relator.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/meta/coinductive_predicates.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/apply_fun.lean : line 8 : ERR_MOD : Module docstring missing, or too late
Expand Down

0 comments on commit 923a14d

Please sign in to comment.