Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#13408)
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 Apr 13, 2022
1 parent b0bd771 commit 1de6ce9
Showing 1 changed file with 0 additions and 5 deletions.
5 changes: 0 additions & 5 deletions scripts/nolints.txt
Expand Up @@ -124,7 +124,6 @@ apply_nolint traversable.free.mk doc_blame
apply_nolint traversable.length doc_blame
apply_nolint traversable.map_fold doc_blame
apply_nolint traversable.mfoldl doc_blame
apply_nolint traversable.mfoldl.unop_of_free_monoid unused_arguments
apply_nolint traversable.mfoldr doc_blame

-- control/monad/cont.lean
Expand Down Expand Up @@ -626,10 +625,6 @@ apply_nolint gaussian_int.mod doc_blame
-- order/filter/at_top_bot.lean
apply_nolint filter.map_at_top_finset_prod_le_of_prod_eq to_additive_doc

-- order/filter/pointwise.lean
apply_nolint filter.has_add check_reducibility
apply_nolint filter.has_mul check_reducibility

-- order/prime_ideal.lean
apply_nolint order.ideal.is_prime.is_maximal fails_quickly

Expand Down

0 comments on commit 1de6ce9

Please sign in to comment.