From 3936f5fdc065a73b6ca9ba03ca1d673850948b57 Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Wed, 17 Mar 2021 02:56:43 +0000 Subject: [PATCH] chore(scripts): update nolints.txt (#6719) I am happy to remove some nolints for you! --- scripts/nolints.txt | 3 --- scripts/style-exceptions.txt | 22 +++++++++------------- 2 files changed, 9 insertions(+), 16 deletions(-) diff --git a/scripts/nolints.txt b/scripts/nolints.txt index 09b1c33cc2769..ff69f81f8ff9b 100644 --- a/scripts/nolints.txt +++ b/scripts/nolints.txt @@ -1132,9 +1132,6 @@ apply_nolint continuous_map.induced doc_blame -- topology/maps.lean apply_nolint inducing doc_blame --- topology/metric_space/emetric_space.lean -apply_nolint has_edist doc_blame - -- topology/metric_space/gluing.lean apply_nolint metric.glue_premetric doc_blame apply_nolint metric.glue_space doc_blame diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt index 5b6d26ddd4dcd..98b041ec831fe 100644 --- a/scripts/style-exceptions.txt +++ b/scripts/style-exceptions.txt @@ -32,7 +32,6 @@ src/category_theory/monad/basic.lean : line 9 : ERR_MOD : Module docstring missi src/category_theory/monad/limits.lean : line 10 : ERR_MOD : Module docstring missing, or too late src/category_theory/natural_transformation.lean : line 16 : ERR_MOD : Module docstring missing, or too late src/category_theory/opposites.lean : line 10 : ERR_MOD : Module docstring missing, or too late -src/category_theory/products/associator.lean : line 8 : ERR_MOD : Module docstring missing, or too late src/category_theory/products/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late src/category_theory/products/bifunctor.lean : line 8 : ERR_MOD : Module docstring missing, or too late src/category_theory/punit.lean : line 9 : ERR_MOD : Module docstring missing, or too late @@ -164,7 +163,7 @@ src/data/seq/computation.lean : line 11 : ERR_MOD : Module docstring missing, or 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/wseq.lean : line 8 : ERR_MOD : Module docstring missing, or too late -src/data/set/basic.lean : line 2435 : ERR_LIN : Line has more than 100 characters +src/data/set/basic.lean : line 2439 : ERR_LIN : Line has more than 100 characters src/data/set/basic.lean : line 897 : ERR_LIN : Line has more than 100 characters src/data/set/disjointed.lean : line 10 : ERR_MOD : Module docstring missing, or too late src/data/set/enumerate.lean : line 10 : ERR_MOD : Module docstring missing, or too late @@ -215,9 +214,9 @@ src/geometry/manifold/local_invariant_properties.lean : line 211 : ERR_LIN : Lin src/geometry/manifold/local_invariant_properties.lean : line 216 : ERR_LIN : Line has more than 100 characters src/geometry/manifold/local_invariant_properties.lean : line 388 : ERR_LIN : Line has more than 100 characters src/geometry/manifold/local_invariant_properties.lean : line 433 : ERR_LIN : Line has more than 100 characters -src/geometry/manifold/times_cont_mdiff.lean : line 1015 : ERR_LIN : Line has more than 100 characters -src/geometry/manifold/times_cont_mdiff.lean : line 1395 : ERR_LIN : Line has more than 100 characters -src/geometry/manifold/times_cont_mdiff.lean : line 1695 : ERR_LIN : Line has more than 100 characters +src/geometry/manifold/times_cont_mdiff.lean : line 1022 : ERR_LIN : Line has more than 100 characters +src/geometry/manifold/times_cont_mdiff.lean : line 1402 : ERR_LIN : Line has more than 100 characters +src/geometry/manifold/times_cont_mdiff.lean : line 1702 : ERR_LIN : Line has more than 100 characters src/geometry/manifold/times_cont_mdiff.lean : line 244 : ERR_LIN : Line has more than 100 characters src/geometry/manifold/times_cont_mdiff.lean : line 298 : ERR_LIN : Line has more than 100 characters src/geometry/manifold/times_cont_mdiff.lean : line 355 : ERR_LIN : Line has more than 100 characters @@ -555,18 +554,15 @@ src/topology/instances/real.lean : line 136 : ERR_LIN : Line has more than 100 c src/topology/local_homeomorph.lean : line 567 : ERR_LIN : Line has more than 100 characters src/topology/local_homeomorph.lean : line 578 : ERR_LIN : Line has more than 100 characters src/topology/metric_space/basic.lean : line 17 : ERR_MOD : Module docstring missing, or too late -src/topology/metric_space/gromov_hausdorff.lean : line 61 : ERR_LIN : Line has more than 100 characters -src/topology/metric_space/isometry.lean : line 385 : ERR_LIN : Line has more than 100 characters +src/topology/metric_space/gromov_hausdorff.lean : line 62 : ERR_LIN : Line has more than 100 characters src/topology/metric_space/premetric_space.lean : line 82 : ERR_LIN : Line has more than 100 characters src/topology/omega_complete_partial_order.lean : line 85 : ERR_LIN : Line has more than 100 characters src/topology/separation.lean : line 11 : ERR_MOD : Module docstring missing, or too late src/topology/sheaves/forget.lean : line 147 : ERR_LIN : Line has more than 100 characters -src/topology/sheaves/presheaf.lean : line 106 : ERR_LIN : Line has more than 100 characters +src/topology/sheaves/presheaf.lean : line 108 : ERR_LIN : Line has more than 100 characters src/topology/sheaves/presheaf.lean : line 40 : ERR_LIN : Line has more than 100 characters -src/topology/sheaves/presheaf.lean : line 57 : ERR_LIN : Line has more than 100 characters -src/topology/sheaves/presheaf.lean : line 58 : ERR_LIN : Line has more than 100 characters -src/topology/sheaves/presheaf.lean : line 94 : ERR_LIN : Line has more than 100 characters -src/topology/sheaves/presheaf.lean : line 97 : ERR_LIN : Line has more than 100 characters +src/topology/sheaves/presheaf.lean : line 96 : ERR_LIN : Line has more than 100 characters +src/topology/sheaves/presheaf.lean : line 99 : ERR_LIN : Line has more than 100 characters src/topology/sheaves/presheaf_of_functions.lean : line 80 : ERR_LIN : Line has more than 100 characters src/topology/sheaves/sheaf.lean : line 89 : ERR_LIN : Line has more than 100 characters src/topology/sheaves/sheaf.lean : line 91 : ERR_LIN : Line has more than 100 characters @@ -576,7 +572,7 @@ src/topology/sheaves/sheaf_of_functions.lean : line 168 : ERR_LIN : Line has mor src/topology/sheaves/stalks.lean : line 11 : ERR_MOD : Module docstring missing, or too late src/topology/sheaves/stalks.lean : line 128 : ERR_LIN : Line has more than 100 characters src/topology/sheaves/stalks.lean : line 133 : ERR_LIN : Line has more than 100 characters -src/topology/subset_properties.lean : line 1097 : ERR_LIN : Line has more than 100 characters +src/topology/subset_properties.lean : line 1113 : ERR_LIN : Line has more than 100 characters src/topology/tactic.lean : line 84 : ERR_LIN : Line has more than 100 characters src/topology/uniform_space/absolute_value.lean : line 71 : ERR_LIN : Line has more than 100 characters src/topology/uniform_space/compact_separated.lean : line 128 : ERR_LIN : Line has more than 100 characters