Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#13964)
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 5, 2022
1 parent 116435d commit 63875ea
Showing 1 changed file with 0 additions and 16 deletions.
16 changes: 0 additions & 16 deletions scripts/nolints.txt
Expand Up @@ -27,26 +27,10 @@ apply_nolint mul_hom.ext_iff to_additive_doc
apply_nolint one_hom.comp_assoc to_additive_doc

-- algebra/order/group.lean
apply_nolint inv_le_of_inv_le' to_additive_doc
apply_nolint inv_lt_of_inv_lt' to_additive_doc
apply_nolint inv_mul_lt_of_lt_mul to_additive_doc
apply_nolint inv_of_one_lt_inv to_additive_doc
apply_nolint le_inv_mul_of_mul_le to_additive_doc
apply_nolint le_inv_of_le_inv to_additive_doc
apply_nolint le_one_of_one_le_inv to_additive_doc
apply_nolint left.inv_le_one_iff to_additive_doc
apply_nolint left.inv_lt_one_iff to_additive_doc
apply_nolint left.one_le_inv_iff to_additive_doc
apply_nolint left.one_lt_inv_iff to_additive_doc
apply_nolint lt_inv_mul_of_mul_lt to_additive_doc
apply_nolint lt_inv_of_lt_inv to_additive_doc
apply_nolint lt_mul_of_inv_mul_lt to_additive_doc
apply_nolint lt_of_inv_lt_inv to_additive_doc
apply_nolint mul_le_of_le_inv_mul to_additive_doc
apply_nolint mul_lt_of_lt_inv_mul to_additive_doc
apply_nolint one_le_of_inv_le_one to_additive_doc
apply_nolint one_lt_inv_of_inv to_additive_doc
apply_nolint one_lt_of_inv_lt_one to_additive_doc
apply_nolint right.inv_le_one_iff to_additive_doc
apply_nolint right.one_le_inv_iff to_additive_doc

Expand Down

0 comments on commit 63875ea

Please sign in to comment.