Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5763)
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
leanprover-community-bot committed Jan 16, 2021
1 parent 6351f01 commit 592edb6
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 22 deletions.
1 change: 0 additions & 1 deletion scripts/nolints.txt
View file
Expand Up @@ -1159,7 +1159,6 @@ apply_nolint continuous_map.induced doc_blame

-- topology/maps.lean
apply_nolint inducing doc_blame
apply_nolint is_closed_map doc_blame

-- topology/metric_space/emetric_space.lean
apply_nolint has_edist doc_blame
Expand Down
42 changes: 21 additions & 21 deletions scripts/style-exceptions.txt
View file
Expand Up @@ -77,7 +77,7 @@ src/algebraic_geometry/sheafed_space.lean : line 50 : ERR_LIN : Line has more th
src/algebraic_geometry/sheafed_space.lean : line 82 : ERR_LIN : Line has more than 100 characters
src/algebraic_geometry/stalks.lean : line 47 : ERR_LIN : Line has more than 100 characters
src/algebraic_geometry/stalks.lean : line 48 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/basic.lean : line 735 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/basic.lean : line 779 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 205 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/deriv.lean : line 1105 : ERR_LIN : Line has more than 100 characters
src/analysis/calculus/local_extr.lean : line 22 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -107,7 +107,7 @@ src/analysis/normed_space/multilinear.lean : line 726 : ERR_LIN : Line has more
src/analysis/normed_space/multilinear.lean : line 898 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 238 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 34 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 645 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 649 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 91 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/arsinh.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/analysis/special_functions/pow.lean : line 1390 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -339,7 +339,7 @@ src/category_theory/monoidal/of_has_finite_products.lean : line 45 : ERR_LIN : L
src/category_theory/natural_transformation.lean : line 16 : ERR_MOD : Module docstring missing, or too late
src/category_theory/natural_transformation.lean : line 18 : ERR_LIN : Line has more than 100 characters
src/category_theory/opposites.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/category_theory/over.lean : line 89 : ERR_LIN : Line has more than 100 characters
src/category_theory/over.lean : line 90 : ERR_LIN : Line has more than 100 characters
src/category_theory/products/associator.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/category_theory/products/basic.lean : line 10 : ERR_LIN : Line has more than 100 characters
src/category_theory/products/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -512,7 +512,7 @@ src/data/matrix/basic.lean : line 500 : ERR_LIN : Line has more than 100 charact
src/data/matrix/basic.lean : line 869 : ERR_LIN : Line has more than 100 characters
src/data/matrix/basic.lean : line 871 : ERR_LIN : Line has more than 100 characters
src/data/matrix/basic.lean : line 924 : ERR_LIN : Line has more than 100 characters
src/data/matrix/notation.lean : line 375 : ERR_LIN : Line has more than 100 characters
src/data/matrix/notation.lean : line 383 : ERR_LIN : Line has more than 100 characters
src/data/matrix/pequiv.lean : line 137 : ERR_LIN : Line has more than 100 characters
src/data/matrix/pequiv.lean : line 143 : ERR_LIN : Line has more than 100 characters
src/data/matrix/pequiv.lean : line 8 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -563,14 +563,14 @@ src/data/mv_polynomial/monad.lean : line 197 : ERR_LIN : Line has more than 100
src/data/mv_polynomial/monad.lean : line 247 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/monad.lean : line 263 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/monad.lean : line 66 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/variables.lean : line 182 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/variables.lean : line 185 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/variables.lean : line 24 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/variables.lean : line 245 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/variables.lean : line 247 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/variables.lean : line 248 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/variables.lean : line 250 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/variables.lean : line 28 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/variables.lean : line 31 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/variables.lean : line 34 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/variables.lean : line 621 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/variables.lean : line 624 : ERR_LIN : Line has more than 100 characters
src/data/nat/basic.lean : line 109 : ERR_LIN : Line has more than 100 characters
src/data/nat/basic.lean : line 870 : ERR_LIN : Line has more than 100 characters
src/data/nat/cast.lean : line 11 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -999,14 +999,14 @@ src/order/filter/bases.lean : line 259 : ERR_LIN : Line has more than 100 charac
src/order/filter/bases.lean : line 40 : ERR_LIN : Line has more than 100 characters
src/order/filter/bases.lean : line 625 : ERR_LIN : Line has more than 100 characters
src/order/filter/bases.lean : line 86 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1377 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1517 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1523 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1540 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1826 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1978 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 2106 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 2351 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1379 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1519 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1525 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1542 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1828 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1980 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 2113 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 2358 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 675 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 685 : ERR_LIN : Line has more than 100 characters
src/order/filter/extr.lean : line 301 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1438,9 +1438,9 @@ src/topology/algebra/continuous_functions.lean : line 87 : ERR_LIN : Line has mo
src/topology/algebra/floor_ring.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/floor_ring.lean : line 183 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/floor_ring.lean : line 187 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 527 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 537 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 556 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 538 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 548 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 567 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group_completion.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/group_completion.lean : line 84 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group_completion.lean : line 90 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1520,8 +1520,8 @@ src/topology/local_extr.lean : line 122 : ERR_LIN : Line has more than 100 chara
src/topology/local_extr.lean : line 255 : ERR_LIN : Line has more than 100 characters
src/topology/local_extr.lean : line 261 : ERR_LIN : Line has more than 100 characters
src/topology/local_extr.lean : line 267 : ERR_LIN : Line has more than 100 characters
src/topology/local_homeomorph.lean : line 503 : ERR_LIN : Line has more than 100 characters
src/topology/local_homeomorph.lean : line 514 : ERR_LIN : Line has more than 100 characters
src/topology/local_homeomorph.lean : line 508 : ERR_LIN : Line has more than 100 characters
src/topology/local_homeomorph.lean : line 519 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 109 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 1321 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/basic.lean : line 15 : ERR_MOD : Module docstring missing, or too late
Expand Down

0 comments on commit 592edb6

Please sign in to comment.