Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5540)
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 Dec 31, 2020
1 parent 9c46cad commit 611b73e
Showing 1 changed file with 30 additions and 31 deletions.
61 changes: 30 additions & 31 deletions scripts/copy-mod-doc-exceptions.txt
View file
Expand Up @@ -138,8 +138,8 @@ src/algebraic_geometry/stalks.lean : line 48 : ERR_LIN : Line has more than 100
src/analysis/analytic/basic.lean : line 206 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/basic.lean : line 349 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/basic.lean : line 574 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/basic.lean : line 686 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/basic.lean : line 766 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/basic.lean : line 683 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/basic.lean : line 763 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 161 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 204 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 242 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -185,12 +185,12 @@ src/analysis/convex/extrema.lean : line 96 : ERR_LIN : Line has more than 100 ch
src/analysis/hofer.lean : line 41 : ERR_LIN : Line has more than 100 characters
src/analysis/mean_inequalities.lean : line 127 : ERR_LIN : Line has more than 100 characters
src/analysis/mean_inequalities.lean : line 338 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/banach.lean : line 184 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/basic.lean : line 1169 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/basic.lean : line 297 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/basic.lean : line 489 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/basic.lean : line 491 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/basic.lean : line 604 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/banach.lean : line 181 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/basic.lean : line 1190 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/basic.lean : line 300 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/basic.lean : line 492 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/basic.lean : line 494 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/basic.lean : line 607 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/basic.lean : line 67 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/bounded_linear_maps.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/analysis/normed_space/bounded_linear_maps.lean : line 154 : ERR_LIN : Line has more than 100 characters
Expand All @@ -200,17 +200,17 @@ src/analysis/normed_space/bounded_linear_maps.lean : line 392 : ERR_LIN : Line h
src/analysis/normed_space/bounded_linear_maps.lean : line 447 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/finite_dimension.lean : line 171 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/finite_dimension.lean : line 262 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1046 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1083 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1280 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1282 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1290 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1314 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1320 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1321 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1387 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1532 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1541 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1061 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1098 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1295 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1297 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1305 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1329 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1335 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1336 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1402 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1547 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 1556 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 348 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 814 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/inner_product.lean : line 833 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -781,7 +781,7 @@ src/data/nat/basic.lean : line 867 : ERR_LIN : Line has more than 100 characters
src/data/nat/cast.lean : line 101 : ERR_LIN : Line has more than 100 characters
src/data/nat/cast.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/nat/dist.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/data/nat/enat.lean : line 309 : ERR_LIN : Line has more than 100 characters
src/data/nat/enat.lean : line 373 : ERR_LIN : Line has more than 100 characters
src/data/nat/gcd.lean : line 182 : ERR_LIN : Line has more than 100 characters
src/data/nat/gcd.lean : line 266 : ERR_LIN : Line has more than 100 characters
src/data/nat/gcd.lean : line 277 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1130,7 +1130,7 @@ src/logic/relation.lean : line 10 : ERR_MOD : Module docstring missing, or too l
src/logic/relator.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/measure_theory/category/Meas.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/measure_theory/decomposition.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/measure_theory/measure_space.lean : line 1720 : ERR_LIN : Line has more than 100 characters
src/measure_theory/measure_space.lean : line 1702 : ERR_LIN : Line has more than 100 characters
src/measure_theory/measure_space.lean : line 65 : ERR_LIN : Line has more than 100 characters
src/meta/coinductive_predicates.lean : line 115 : ERR_LIN : Line has more than 100 characters
src/meta/coinductive_predicates.lean : line 12 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1353,9 +1353,8 @@ src/ring_theory/localization.lean : line 1364 : ERR_LIN : Line has more than 100
src/ring_theory/localization.lean : line 1552 : ERR_LIN : Line has more than 100 characters
src/ring_theory/localization.lean : line 873 : ERR_LIN : Line has more than 100 characters
src/ring_theory/multiplicity.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/ring_theory/multiplicity.lean : line 142 : ERR_LIN : Line has more than 100 characters
src/ring_theory/multiplicity.lean : line 321 : ERR_LIN : Line has more than 100 characters
src/ring_theory/multiplicity.lean : line 322 : ERR_LIN : Line has more than 100 characters
src/ring_theory/multiplicity.lean : line 313 : ERR_LIN : Line has more than 100 characters
src/ring_theory/multiplicity.lean : line 314 : ERR_LIN : Line has more than 100 characters
src/ring_theory/noetherian.lean : line 178 : ERR_LIN : Line has more than 100 characters
src/ring_theory/noetherian.lean : line 372 : ERR_LIN : Line has more than 100 characters
src/ring_theory/noetherian.lean : line 392 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1492,8 +1491,8 @@ src/tactic/linarith/datatypes.lean : line 276 : ERR_LIN : Line has more than 100
src/tactic/linarith/datatypes.lean : line 301 : ERR_LIN : Line has more than 100 characters
src/tactic/linarith/elimination.lean : line 121 : ERR_LIN : Line has more than 100 characters
src/tactic/linarith/frontend.lean : line 156 : ERR_LIN : Line has more than 100 characters
src/tactic/linarith/frontend.lean : line 250 : ERR_LIN : Line has more than 100 characters
src/tactic/linarith/frontend.lean : line 256 : ERR_LIN : Line has more than 100 characters
src/tactic/linarith/frontend.lean : line 251 : ERR_LIN : Line has more than 100 characters
src/tactic/linarith/frontend.lean : line 257 : ERR_LIN : Line has more than 100 characters
src/tactic/linarith/frontend.lean : line 259 : ERR_LIN : Line has more than 100 characters
src/tactic/linarith/frontend.lean : line 260 : ERR_LIN : Line has more than 100 characters
src/tactic/linarith/lemmas.lean : line 22 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1696,15 +1695,15 @@ 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 516 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 526 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 545 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 509 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group.lean : line 519 : 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_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
src/topology/algebra/group_completion.lean : line 97 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group_completion.lean : line 99 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/infinite_sum.lean : line 713 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/infinite_sum.lean : line 725 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 1080 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 1090 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 300 : ERR_LIN : Line has more than 100 characters
Expand All @@ -1717,7 +1716,7 @@ src/topology/algebra/multilinear.lean : line 245 : ERR_LIN : Line has more than
src/topology/algebra/multilinear.lean : line 46 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/multilinear.lean : line 60 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/open_subgroup.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/ordered.lean : line 1666 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 1762 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 41 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 430 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 434 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit 611b73e

Please sign in to comment.