chore(scripts): update nolints.txt (#16244)

I am happy to remove some nolints for you!
leanprover-community · Aug 25, 2022 · b6931e1 · b6931e1
1 parent c5be877
commit b6931e1
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 7 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -214,12 +214,6 @@ apply_nolint add_monoid_hom.pi_ext fintype_finite
 apply_nolint finset.noncomm_prod_union_of_disjoint to_additive_doc
 apply_nolint monoid_hom.pi_ext fintype_finite
 
--- data/finset/pi_induction.lean
-apply_nolint finset.induction_on_pi fintype_finite
-apply_nolint finset.induction_on_pi_max fintype_finite
-apply_nolint finset.induction_on_pi_min fintype_finite
-apply_nolint finset.induction_on_pi_of_choice fintype_finite
-
 -- data/finsupp/pwo.lean
 apply_nolint finsupp.is_pwo fintype_finite
 

diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt
@@ -20,7 +20,7 @@ src/data/rbtree/main.lean : line 11 : ERR_MOD : Module docstring missing, or too
 src/data/rbtree/min_max.lean : line 7 : ERR_MOD : Module docstring missing, or too late
 src/data/seq/computation.lean : line 12 : ERR_MOD : Module docstring missing, or too late
 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/seq.lean : line 12 : ERR_MOD : Module docstring missing, or too late
 src/data/seq/wseq.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