From 7500b242f24f385662c5315e68b818d9de870578 Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Fri, 8 Jan 2021 02:05:16 +0000 Subject: [PATCH] chore(scripts): update nolints.txt (#5661) I am happy to remove some nolints for you! --- scripts/style-exceptions.txt | 108 +++++++++++++++-------------------- 1 file changed, 47 insertions(+), 61 deletions(-) diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt index 4aba13e9c665a..d36a1b6f73f61 100644 --- a/scripts/style-exceptions.txt +++ b/scripts/style-exceptions.txt @@ -19,7 +19,7 @@ archive/sensitivity.lean : line 414 : ERR_LIN : Line has more than 100 character archive/sensitivity.lean : line 415 : ERR_LIN : Line has more than 100 characters archive/sensitivity.lean : line 416 : ERR_LIN : Line has more than 100 characters archive/sensitivity.lean : line 420 : ERR_LIN : Line has more than 100 characters -src/algebra/algebra/subalgebra.lean : line 393 : ERR_LIN : Line has more than 100 characters +src/algebra/algebra/subalgebra.lean : line 408 : ERR_LIN : Line has more than 100 characters src/algebra/archimedean.lean : line 11 : ERR_MOD : Module docstring missing, or too late src/algebra/category/Algebra/basic.lean : line 12 : ERR_MOD : Module docstring missing, or too late src/algebra/category/CommRing/basic.lean : line 157 : ERR_LIN : Line has more than 100 characters @@ -147,13 +147,13 @@ src/analysis/analytic/composition.lean : line 854 : ERR_LIN : Line has more than src/analysis/analytic/composition.lean : line 894 : ERR_LIN : Line has more than 100 characters src/analysis/calculus/deriv.lean : line 1104 : ERR_LIN : Line has more than 100 characters src/analysis/calculus/deriv.lean : line 326 : ERR_LIN : Line has more than 100 characters -src/analysis/calculus/fderiv.lean : line 1928 : ERR_LIN : Line has more than 100 characters +src/analysis/calculus/fderiv.lean : line 1932 : ERR_LIN : Line has more than 100 characters src/analysis/calculus/fderiv.lean : line 206 : ERR_LIN : Line has more than 100 characters -src/analysis/calculus/fderiv.lean : line 2352 : ERR_LIN : Line has more than 100 characters -src/analysis/calculus/fderiv.lean : line 2536 : ERR_LIN : Line has more than 100 characters +src/analysis/calculus/fderiv.lean : line 2356 : ERR_LIN : Line has more than 100 characters +src/analysis/calculus/fderiv.lean : line 2540 : ERR_LIN : Line has more than 100 characters src/analysis/calculus/fderiv.lean : line 308 : ERR_LIN : Line has more than 100 characters src/analysis/calculus/fderiv.lean : line 405 : ERR_LIN : Line has more than 100 characters -src/analysis/calculus/fderiv.lean : line 975 : ERR_LIN : Line has more than 100 characters +src/analysis/calculus/fderiv.lean : line 979 : ERR_LIN : Line has more than 100 characters src/analysis/calculus/iterated_deriv.lean : line 122 : ERR_LIN : Line has more than 100 characters src/analysis/calculus/iterated_deriv.lean : line 77 : ERR_LIN : Line has more than 100 characters src/analysis/calculus/local_extr.lean : line 22 : ERR_LIN : Line has more than 100 characters @@ -174,9 +174,6 @@ src/analysis/calculus/times_cont_diff.lean : line 525 : ERR_LIN : Line has more src/analysis/calculus/times_cont_diff.lean : line 689 : ERR_LIN : Line has more than 100 characters src/analysis/calculus/times_cont_diff.lean : line 846 : ERR_LIN : Line has more than 100 characters src/analysis/complex/polynomial.lean : line 50 : ERR_LIN : Line has more than 100 characters -src/analysis/convex/basic.lean : line 1130 : ERR_LIN : Line has more than 100 characters -src/analysis/convex/basic.lean : line 1190 : ERR_LIN : Line has more than 100 characters -src/analysis/convex/basic.lean : line 728 : ERR_LIN : Line has more than 100 characters src/analysis/convex/caratheodory.lean : line 76 : ERR_LIN : Line has more than 100 characters src/analysis/convex/extrema.lean : line 50 : ERR_LIN : Line has more than 100 characters src/analysis/convex/extrema.lean : line 96 : ERR_LIN : Line has more than 100 characters @@ -185,11 +182,11 @@ src/analysis/mean_inequalities.lean : line 127 : ERR_LIN : Line has more than 10 src/analysis/mean_inequalities.lean : line 338 : ERR_LIN : Line has more than 100 characters src/analysis/mean_inequalities.lean : line 637 : 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 1230 : ERR_LIN : Line has more than 100 characters -src/analysis/normed_space/basic.lean : line 330 : ERR_LIN : Line has more than 100 characters -src/analysis/normed_space/basic.lean : line 522 : ERR_LIN : Line has more than 100 characters -src/analysis/normed_space/basic.lean : line 524 : ERR_LIN : Line has more than 100 characters -src/analysis/normed_space/basic.lean : line 637 : ERR_LIN : Line has more than 100 characters +src/analysis/normed_space/basic.lean : line 1233 : ERR_LIN : Line has more than 100 characters +src/analysis/normed_space/basic.lean : line 333 : ERR_LIN : Line has more than 100 characters +src/analysis/normed_space/basic.lean : line 525 : ERR_LIN : Line has more than 100 characters +src/analysis/normed_space/basic.lean : line 527 : ERR_LIN : Line has more than 100 characters +src/analysis/normed_space/basic.lean : line 640 : 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 @@ -197,8 +194,8 @@ src/analysis/normed_space/bounded_linear_maps.lean : line 165 : ERR_LIN : Line h src/analysis/normed_space/bounded_linear_maps.lean : line 261 : ERR_LIN : Line has more than 100 characters src/analysis/normed_space/bounded_linear_maps.lean : line 392 : ERR_LIN : Line has more than 100 characters 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 284 : ERR_LIN : Line has more than 100 characters +src/analysis/normed_space/finite_dimension.lean : line 177 : ERR_LIN : Line has more than 100 characters +src/analysis/normed_space/finite_dimension.lean : line 290 : ERR_LIN : Line has more than 100 characters src/analysis/normed_space/inner_product.lean : line 1123 : ERR_LIN : Line has more than 100 characters src/analysis/normed_space/inner_product.lean : line 1489 : ERR_LIN : Line has more than 100 characters src/analysis/normed_space/inner_product.lean : line 1491 : ERR_LIN : Line has more than 100 characters @@ -241,22 +238,11 @@ src/analysis/special_functions/trigonometric.lean : line 1446 : ERR_LIN : Line h 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 1641 : 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 1644 : 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 1675 : ERR_LIN : Line has more than 100 characters -src/analysis/special_functions/trigonometric.lean : line 1678 : ERR_LIN : Line has more than 100 characters -src/analysis/special_functions/trigonometric.lean : line 1692 : ERR_LIN : Line has more than 100 characters -src/analysis/special_functions/trigonometric.lean : line 1702 : ERR_LIN : Line has more than 100 characters -src/analysis/special_functions/trigonometric.lean : line 1763 : ERR_LIN : Line has more than 100 characters -src/analysis/special_functions/trigonometric.lean : line 1814 : ERR_LIN : Line has more than 100 characters -src/analysis/special_functions/trigonometric.lean : line 1864 : ERR_LIN : Line has more than 100 characters -src/analysis/special_functions/trigonometric.lean : line 1936 : ERR_LIN : Line has more than 100 characters -src/analysis/special_functions/trigonometric.lean : line 2119 : ERR_LIN : Line has more than 100 characters -src/analysis/special_functions/trigonometric.lean : line 2415 : ERR_LIN : Line has more than 100 characters -src/analysis/special_functions/trigonometric.lean : line 2459 : ERR_LIN : Line has more than 100 characters +src/analysis/special_functions/trigonometric.lean : line 2034 : ERR_LIN : Line has more than 100 characters +src/analysis/special_functions/trigonometric.lean : line 2084 : ERR_LIN : Line has more than 100 characters +src/analysis/special_functions/trigonometric.lean : line 2156 : ERR_LIN : Line has more than 100 characters +src/analysis/special_functions/trigonometric.lean : line 2339 : ERR_LIN : Line has more than 100 characters +src/analysis/special_functions/trigonometric.lean : line 2750 : ERR_LIN : Line has more than 100 characters src/analysis/specific_limits.lean : line 84 : 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 @@ -275,7 +261,7 @@ src/category_theory/adjunction/limits.lean : line 42 : ERR_LIN : Line has more t src/category_theory/adjunction/limits.lean : line 50 : ERR_LIN : Line has more than 100 characters 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/closed/cartesian.lean : line 329 : ERR_LIN : Line has more than 100 characters +src/category_theory/closed/cartesian.lean : line 332 : ERR_LIN : Line has more than 100 characters src/category_theory/comma.lean : line 47 : ERR_LIN : Line has more than 100 characters src/category_theory/concrete_category/basic.lean : line 112 : ERR_LIN : Line has more than 100 characters src/category_theory/concrete_category/basic.lean : line 116 : ERR_LIN : Line has more than 100 characters @@ -399,13 +385,13 @@ src/category_theory/limits/shapes/binary_products.lean : line 250 : ERR_LIN : Li src/category_theory/limits/shapes/binary_products.lean : line 350 : ERR_LIN : Line has more than 100 characters src/category_theory/limits/shapes/binary_products.lean : line 355 : ERR_LIN : Line has more than 100 characters src/category_theory/limits/shapes/binary_products.lean : line 372 : ERR_LIN : Line has more than 100 characters -src/category_theory/limits/shapes/binary_products.lean : line 400 : ERR_LIN : Line has more than 100 characters -src/category_theory/limits/shapes/binary_products.lean : line 418 : ERR_LIN : Line has more than 100 characters -src/category_theory/limits/shapes/binary_products.lean : line 472 : ERR_LIN : Line has more than 100 characters -src/category_theory/limits/shapes/binary_products.lean : line 496 : ERR_LIN : Line has more than 100 characters -src/category_theory/limits/shapes/binary_products.lean : line 502 : ERR_LIN : Line has more than 100 characters -src/category_theory/limits/shapes/binary_products.lean : line 667 : ERR_LIN : Line has more than 100 characters -src/category_theory/limits/shapes/binary_products.lean : line 738 : ERR_LIN : Line has more than 100 characters +src/category_theory/limits/shapes/binary_products.lean : line 404 : ERR_LIN : Line has more than 100 characters +src/category_theory/limits/shapes/binary_products.lean : line 422 : ERR_LIN : Line has more than 100 characters +src/category_theory/limits/shapes/binary_products.lean : line 476 : ERR_LIN : Line has more than 100 characters +src/category_theory/limits/shapes/binary_products.lean : line 504 : ERR_LIN : Line has more than 100 characters +src/category_theory/limits/shapes/binary_products.lean : line 510 : ERR_LIN : Line has more than 100 characters +src/category_theory/limits/shapes/binary_products.lean : line 675 : ERR_LIN : Line has more than 100 characters +src/category_theory/limits/shapes/binary_products.lean : line 746 : ERR_LIN : Line has more than 100 characters src/category_theory/limits/shapes/binary_products.lean : line 84 : ERR_LIN : Line has more than 100 characters src/category_theory/limits/shapes/binary_products.lean : line 86 : ERR_LIN : Line has more than 100 characters src/category_theory/limits/shapes/binary_products.lean : line 92 : ERR_LIN : Line has more than 100 characters @@ -485,10 +471,10 @@ src/category_theory/monad/algebra.lean : line 135 : ERR_LIN : Line has more than src/category_theory/monad/algebra.lean : line 211 : ERR_LIN : Line has more than 100 characters src/category_theory/monad/algebra.lean : line 216 : ERR_LIN : Line has more than 100 characters src/category_theory/monad/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late -src/category_theory/monad/limits.lean : line 107 : ERR_LIN : Line has more than 100 characters -src/category_theory/monad/limits.lean : line 188 : ERR_LIN : Line has more than 100 characters -src/category_theory/monad/limits.lean : line 215 : ERR_LIN : Line has more than 100 characters -src/category_theory/monad/limits.lean : line 9 : ERR_MOD : Module docstring missing, or too late +src/category_theory/monad/limits.lean : line 10 : ERR_MOD : Module docstring missing, or too late +src/category_theory/monad/limits.lean : line 108 : ERR_LIN : Line has more than 100 characters +src/category_theory/monad/limits.lean : line 189 : ERR_LIN : Line has more than 100 characters +src/category_theory/monad/limits.lean : line 216 : ERR_LIN : Line has more than 100 characters src/category_theory/monoidal/CommMon_.lean : line 139 : ERR_LIN : Line has more than 100 characters src/category_theory/monoidal/Mon_.lean : line 55 : ERR_LIN : Line has more than 100 characters src/category_theory/monoidal/braided.lean : line 217 : ERR_LIN : Line has more than 100 characters @@ -951,7 +937,7 @@ src/field_theory/intermediate_field.lean : line 155 : ERR_LIN : Line has more th src/field_theory/minimal_polynomial.lean : line 102 : ERR_LIN : Line has more than 100 characters src/field_theory/minimal_polynomial.lean : line 250 : ERR_LIN : Line has more than 100 characters src/field_theory/minimal_polynomial.lean : line 319 : ERR_LIN : Line has more than 100 characters -src/field_theory/mv_polynomial.lean : line 13 : ERR_MOD : Module docstring missing, or too late +src/field_theory/mv_polynomial.lean : line 14 : ERR_MOD : Module docstring missing, or too late src/field_theory/primitive_element.lean : line 29 : ERR_LIN : Line has more than 100 characters src/field_theory/splitting_field.lean : line 16 : ERR_MOD : Module docstring missing, or too late src/field_theory/splitting_field.lean : line 378 : ERR_LIN : Line has more than 100 characters @@ -965,11 +951,11 @@ src/field_theory/splitting_field.lean : line 77 : ERR_LIN : Line has more than 1 src/field_theory/splitting_field.lean : line 78 : ERR_LIN : Line has more than 100 characters src/field_theory/subfield.lean : line 449 : ERR_LIN : Line has more than 100 characters src/geometry/euclidean/basic.lean : line 13 : ERR_MOD : Module docstring missing, or too late -src/geometry/euclidean/basic.lean : line 196 : ERR_LIN : Line has more than 100 characters -src/geometry/euclidean/basic.lean : line 440 : ERR_LIN : Line has more than 100 characters -src/geometry/euclidean/basic.lean : line 550 : ERR_LIN : Line has more than 100 characters -src/geometry/euclidean/basic.lean : line 566 : ERR_LIN : Line has more than 100 characters -src/geometry/euclidean/basic.lean : line 914 : ERR_LIN : Line has more than 100 characters +src/geometry/euclidean/basic.lean : line 189 : ERR_LIN : Line has more than 100 characters +src/geometry/euclidean/basic.lean : line 391 : ERR_LIN : Line has more than 100 characters +src/geometry/euclidean/basic.lean : line 501 : ERR_LIN : Line has more than 100 characters +src/geometry/euclidean/basic.lean : line 517 : ERR_LIN : Line has more than 100 characters +src/geometry/euclidean/basic.lean : line 865 : ERR_LIN : Line has more than 100 characters src/geometry/euclidean/circumcenter.lean : line 10 : ERR_MOD : Module docstring missing, or too late src/geometry/euclidean/circumcenter.lean : line 544 : ERR_LIN : Line has more than 100 characters src/geometry/euclidean/circumcenter.lean : line 841 : ERR_LIN : Line has more than 100 characters @@ -1085,8 +1071,8 @@ src/group_theory/presented_group.lean : line 51 : ERR_LIN : Line has more than 1 src/group_theory/quotient_group.lean : line 10 : ERR_MOD : Module docstring missing, or too late src/group_theory/semidirect_product.lean : line 52 : ERR_LIN : Line has more than 100 characters src/group_theory/subgroup.lean : line 377 : ERR_LIN : Line has more than 100 characters -src/group_theory/subgroup.lean : line 814 : ERR_LIN : Line has more than 100 characters -src/group_theory/subgroup.lean : line 849 : ERR_LIN : Line has more than 100 characters +src/group_theory/subgroup.lean : line 826 : ERR_LIN : Line has more than 100 characters +src/group_theory/subgroup.lean : line 861 : ERR_LIN : Line has more than 100 characters src/group_theory/submonoid/operations.lean : line 560 : ERR_LIN : Line has more than 100 characters src/group_theory/sylow.lean : line 13 : ERR_MOD : Module docstring missing, or too late src/linear_algebra/basis.lean : line 291 : ERR_LIN : Line has more than 100 characters @@ -1301,7 +1287,7 @@ src/ring_theory/free_comm_ring.lean : line 263 : ERR_LIN : Line has more than 10 src/ring_theory/free_ring.lean : line 83 : ERR_LIN : Line has more than 100 characters src/ring_theory/free_ring.lean : line 86 : ERR_LIN : Line has more than 100 characters src/ring_theory/ideal/basic.lean : line 63 : ERR_LIN : Line has more than 100 characters -src/ring_theory/ideal/operations.lean : line 1264 : ERR_LIN : Line has more than 100 characters +src/ring_theory/ideal/operations.lean : line 1269 : ERR_LIN : Line has more than 100 characters src/ring_theory/ideal/operations.lean : line 138 : ERR_LIN : Line has more than 100 characters src/ring_theory/ideal/operations.lean : line 142 : ERR_LIN : Line has more than 100 characters src/ring_theory/ideal/operations.lean : line 143 : ERR_LIN : Line has more than 100 characters @@ -1319,7 +1305,7 @@ src/ring_theory/ideal/operations.lean : line 568 : ERR_LIN : Line has more than src/ring_theory/ideal/operations.lean : line 865 : ERR_LIN : Line has more than 100 characters src/ring_theory/ideal/operations.lean : line 93 : ERR_LIN : Line has more than 100 characters src/ring_theory/ideal/operations.lean : line 95 : ERR_LIN : Line has more than 100 characters -src/ring_theory/ideal/operations.lean : line 991 : ERR_LIN : Line has more than 100 characters +src/ring_theory/ideal/operations.lean : line 996 : ERR_LIN : Line has more than 100 characters src/ring_theory/integral_closure.lean : line 118 : ERR_LIN : Line has more than 100 characters src/ring_theory/integral_closure.lean : line 123 : ERR_LIN : Line has more than 100 characters src/ring_theory/integral_closure.lean : line 199 : ERR_LIN : Line has more than 100 characters @@ -1334,14 +1320,14 @@ src/ring_theory/jacobson.lean : line 228 : ERR_LIN : Line has more than 100 char src/ring_theory/jacobson.lean : line 363 : ERR_LIN : Line has more than 100 characters src/ring_theory/jacobson.lean : line 366 : ERR_LIN : Line has more than 100 characters src/ring_theory/jacobson.lean : line 88 : ERR_LIN : Line has more than 100 characters -src/ring_theory/jacobson_ideal.lean : line 148 : ERR_LIN : Line has more than 100 characters -src/ring_theory/jacobson_ideal.lean : line 248 : ERR_LIN : Line has more than 100 characters -src/ring_theory/jacobson_ideal.lean : line 279 : ERR_LIN : Line has more than 100 characters -src/ring_theory/jacobson_ideal.lean : line 291 : ERR_LIN : Line has more than 100 characters -src/ring_theory/jacobson_ideal.lean : line 295 : ERR_LIN : Line has more than 100 characters -src/ring_theory/jacobson_ideal.lean : line 67 : ERR_LIN : Line has more than 100 characters -src/ring_theory/jacobson_ideal.lean : line 87 : ERR_LIN : Line has more than 100 characters -src/ring_theory/jacobson_ideal.lean : line 97 : ERR_LIN : Line has more than 100 characters +src/ring_theory/jacobson_ideal.lean : line 150 : ERR_LIN : Line has more than 100 characters +src/ring_theory/jacobson_ideal.lean : line 255 : ERR_LIN : Line has more than 100 characters +src/ring_theory/jacobson_ideal.lean : line 286 : ERR_LIN : Line has more than 100 characters +src/ring_theory/jacobson_ideal.lean : line 298 : ERR_LIN : Line has more than 100 characters +src/ring_theory/jacobson_ideal.lean : line 302 : ERR_LIN : Line has more than 100 characters +src/ring_theory/jacobson_ideal.lean : line 70 : ERR_LIN : Line has more than 100 characters +src/ring_theory/jacobson_ideal.lean : line 89 : ERR_LIN : Line has more than 100 characters +src/ring_theory/jacobson_ideal.lean : line 99 : ERR_LIN : Line has more than 100 characters src/ring_theory/localization.lean : line 1191 : ERR_LIN : Line has more than 100 characters src/ring_theory/localization.lean : line 1215 : ERR_LIN : Line has more than 100 characters src/ring_theory/localization.lean : line 1364 : ERR_LIN : Line has more than 100 characters