Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5433)
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 19, 2020
1 parent ec1b70e commit 53354e7
Showing 1 changed file with 43 additions and 51 deletions.
94 changes: 43 additions & 51 deletions scripts/copy-mod-doc-exceptions.txt
View file
Expand Up @@ -203,11 +203,11 @@ 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 1139 : 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 459 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/basic.lean : line 461 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/basic.lean : line 574 : 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/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 Down Expand Up @@ -248,43 +248,36 @@ src/analysis/special_functions/pow.lean : line 1357 : ERR_LIN : Line has more th
src/analysis/special_functions/pow.lean : line 295 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 296 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 548 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1017 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1051 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 106 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1071 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1076 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1050 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1083 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1125 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1128 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1130 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 131 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1436 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1450 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1453 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1456 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1467 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1471 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1483 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1491 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1656 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1657 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1659 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1688 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 132 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1426 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1440 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1443 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1446 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1457 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1461 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1473 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1481 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1639 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1640 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1642 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1671 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1673 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1676 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1690 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1693 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1707 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1717 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1778 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1829 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1879 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1951 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2134 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2215 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2218 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2325 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2328 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1700 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1761 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1812 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1862 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1934 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2117 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2180 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2183 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2281 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2284 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2380 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2424 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2468 : ERR_LIN : Line has more than 100 characters
src/analysis/specific_limits.lean : line 567 : ERR_LIN : Line has more than 100 characters
src/category_theory/abelian/exact.lean : line 70 : ERR_LIN : Line has more than 100 characters
src/category_theory/abelian/exact.lean : line 76 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -912,12 +905,12 @@ 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 2335 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 472 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 557 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 664 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 759 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 958 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 2344 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 474 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 559 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 668 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 763 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 962 : ERR_LIN : Line has more than 100 characters
src/data/set/countable.lean : line 122 : ERR_LIN : Line has more than 100 characters
src/data/set/countable.lean : line 138 : ERR_LIN : Line has more than 100 characters
src/data/set/disjointed.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -1007,7 +1000,6 @@ src/geometry/euclidean/circumcenter.lean : line 842 : ERR_LIN : Line has more th
src/geometry/euclidean/circumcenter.lean : line 846 : ERR_LIN : Line has more than 100 characters
src/geometry/euclidean/monge_point.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/geometry/euclidean/triangle.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/geometry/euclidean/triangle.lean : line 99 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/algebra/monoid.lean : line 107 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/algebra/monoid.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/geometry/manifold/algebra/structures.lean : line 7 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -1234,10 +1226,10 @@ src/order/bounded_lattice.lean : line 238 : ERR_LIN : Line has more than 100 cha
src/order/complete_boolean_algebra.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/order/complete_lattice.lean : line 201 : ERR_LIN : Line has more than 100 characters
src/order/complete_lattice.lean : line 204 : ERR_LIN : Line has more than 100 characters
src/order/conditionally_complete_lattice.lean : line 485 : ERR_LIN : Line has more than 100 characters
src/order/conditionally_complete_lattice.lean : line 707 : ERR_LIN : Line has more than 100 characters
src/order/conditionally_complete_lattice.lean : line 719 : ERR_LIN : Line has more than 100 characters
src/order/conditionally_complete_lattice.lean : line 850 : ERR_LIN : Line has more than 100 characters
src/order/conditionally_complete_lattice.lean : line 499 : ERR_LIN : Line has more than 100 characters
src/order/conditionally_complete_lattice.lean : line 721 : ERR_LIN : Line has more than 100 characters
src/order/conditionally_complete_lattice.lean : line 733 : ERR_LIN : Line has more than 100 characters
src/order/conditionally_complete_lattice.lean : line 864 : ERR_LIN : Line has more than 100 characters
src/order/directed.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/order/filter/bases.lean : line 251 : ERR_LIN : Line has more than 100 characters
src/order/filter/bases.lean : line 259 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1416,7 +1408,7 @@ src/ring_theory/subring.lean : line 481 : ERR_LIN : Line has more than 100 chara
src/ring_theory/subring.lean : line 484 : ERR_LIN : Line has more than 100 characters
src/ring_theory/subring.lean : line 743 : ERR_LIN : Line has more than 100 characters
src/ring_theory/tensor_product.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/ring_theory/tensor_product.lean : line 490 : ERR_LIN : Line has more than 100 characters
src/ring_theory/tensor_product.lean : line 489 : ERR_LIN : Line has more than 100 characters
src/ring_theory/unique_factorization_domain.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/ring_theory/unique_factorization_domain.lean : line 111 : ERR_LIN : Line has more than 100 characters
src/ring_theory/unique_factorization_domain.lean : line 136 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1749,7 +1741,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 1678 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/ordered.lean : line 1666 : 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 53354e7

Please sign in to comment.