Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#12971)
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 Mar 27, 2022
1 parent 664247f commit 57a5fd7
Showing 1 changed file with 16 additions and 16 deletions.
32 changes: 16 additions & 16 deletions scripts/nolints.txt
Expand Up @@ -15,6 +15,17 @@ apply_nolint free_algebra.semiring check_reducibility
apply_nolint semiconj_by.one_left to_additive_doc
apply_nolint semiconj_by.one_right to_additive_doc

-- algebra/hom/equiv.lean
apply_nolint equiv.mul_left_symm_apply to_additive_doc
apply_nolint equiv.mul_right_symm_apply to_additive_doc
apply_nolint mul_equiv.apply_symm_apply to_additive_doc
apply_nolint mul_equiv.map_div to_additive_doc
apply_nolint mul_equiv.map_inv to_additive_doc
apply_nolint mul_equiv.map_mul to_additive_doc
apply_nolint mul_equiv.map_one to_additive_doc
apply_nolint mul_equiv.symm_apply_apply to_additive_doc
apply_nolint mul_equiv.unique to_additive_doc

-- algebra/hom/freiman.lean
apply_nolint freiman_hom.has_coe_to_fun to_additive_doc

Expand Down Expand Up @@ -217,22 +228,6 @@ apply_nolint ctop.realizer.of_equiv doc_blame
apply_nolint ctop.to_realizer doc_blame
apply_nolint locally_finite.realizer doc_blame has_inhabited_instance

-- data/equiv/list.lean
apply_nolint encodable.fintype_arrow doc_blame
apply_nolint encodable.fintype_pi doc_blame
apply_nolint encodable.trunc_encodable_of_fintype doc_blame

-- data/equiv/mul_add.lean
apply_nolint equiv.mul_left_symm_apply to_additive_doc
apply_nolint equiv.mul_right_symm_apply to_additive_doc
apply_nolint mul_equiv.apply_symm_apply to_additive_doc
apply_nolint mul_equiv.map_div to_additive_doc
apply_nolint mul_equiv.map_inv to_additive_doc
apply_nolint mul_equiv.map_mul to_additive_doc
apply_nolint mul_equiv.map_one to_additive_doc
apply_nolint mul_equiv.symm_apply_apply to_additive_doc
apply_nolint mul_equiv.unique to_additive_doc

-- data/finset/noncomm_prod.lean
apply_nolint finset.noncomm_prod_union_of_disjoint to_additive_doc

Expand Down Expand Up @@ -551,6 +546,11 @@ apply_nolint affine_subspace.to_add_torsor fails_quickly
apply_nolint function.has_scalar to_additive_doc
apply_nolint function.smul_comm_class to_additive_doc

-- logic/equiv/list.lean
apply_nolint encodable.fintype_arrow doc_blame
apply_nolint encodable.fintype_pi doc_blame
apply_nolint encodable.trunc_encodable_of_fintype doc_blame

-- logic/relator.lean
apply_nolint relator.bi_total doc_blame
apply_nolint relator.bi_unique doc_blame
Expand Down

0 comments on commit 57a5fd7

Please sign in to comment.