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

I am happy to remove some nolints for you!
leanprover-community · Jul 10, 2021 · b52c1f0 · b52c1f0
1 parent 70320f7
commit b52c1f0
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 7 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -1,12 +1,6 @@
 import .all
 run_cmd tactic.skip
 
--- category_theory/category/Kleisli.lean
-apply_nolint category_theory.Kleisli doc_blame unused_arguments has_inhabited_instance
-apply_nolint category_theory.Kleisli.comp_def unused_arguments
-apply_nolint category_theory.Kleisli.id_def unused_arguments
-apply_nolint category_theory.Kleisli.mk doc_blame has_inhabited_instance
-
 -- computability/partrec.lean
 apply_nolint computable doc_blame
 apply_nolint computable₂ doc_blame

diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt
@@ -3,7 +3,6 @@ src/analysis/normed_space/bounded_linear_maps.lean : line 10 : ERR_MOD : Module
 src/category_theory/adjunction/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
 src/category_theory/adjunction/fully_faithful.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/category_theory/adjunction/limits.lean : line 9 : ERR_MOD : Module docstring missing, or too late
-src/category_theory/category/Kleisli.lean : line 12 : ERR_MOD : Module docstring missing, or too late
 src/category_theory/endomorphism.lean : line 11 : ERR_MOD : Module docstring missing, or too late
 src/category_theory/epi_mono.lean : line 15 : ERR_MOD : Module docstring missing, or too late
 src/category_theory/eq_to_hom.lean : line 8 : ERR_MOD : Module docstring missing, or too late