From 1de6ce93c44bd9b9a71bc5c967bd24de04ee1af7 Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Wed, 13 Apr 2022 04:14:04 +0000 Subject: [PATCH] chore(scripts): update nolints.txt (#13408) I am happy to remove some nolints for you! --- scripts/nolints.txt | 5 ----- 1 file changed, 5 deletions(-) diff --git a/scripts/nolints.txt b/scripts/nolints.txt index 9360c9c398fb6..101eef31ec2a5 100644 --- a/scripts/nolints.txt +++ b/scripts/nolints.txt @@ -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 @@ -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