From a9fb069baa9e7c6816995feb9e93657b94539e4e Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Sun, 20 Dec 2020 01:39:55 +0000 Subject: [PATCH] chore(scripts): update nolints.txt (#5441) I am happy to remove some nolints for you! --- scripts/copy-mod-doc-exceptions.txt | 78 ++++++++++++++--------------- 1 file changed, 37 insertions(+), 41 deletions(-) diff --git a/scripts/copy-mod-doc-exceptions.txt b/scripts/copy-mod-doc-exceptions.txt index acc6ba261b2c2..f94a772dfd7f7 100644 --- a/scripts/copy-mod-doc-exceptions.txt +++ b/scripts/copy-mod-doc-exceptions.txt @@ -132,8 +132,8 @@ src/algebra/monoid_algebra.lean : line 776 : ERR_LIN : Line has more than 100 ch src/algebra/monoid_algebra.lean : line 832 : ERR_LIN : Line has more than 100 characters src/algebra/monoid_algebra.lean : line 841 : ERR_LIN : Line has more than 100 characters src/algebra/monoid_algebra.lean : line 852 : ERR_LIN : Line has more than 100 characters -src/algebra/ordered_group.lean : line 369 : ERR_LIN : Line has more than 100 characters -src/algebra/ordered_group.lean : line 371 : ERR_LIN : Line has more than 100 characters +src/algebra/ordered_group.lean : line 373 : ERR_LIN : Line has more than 100 characters +src/algebra/ordered_group.lean : line 375 : ERR_LIN : Line has more than 100 characters src/algebra/ordered_group.lean : line 8 : ERR_MOD : Module docstring missing, or too late src/algebra/ordered_ring.lean : line 9 : ERR_MOD : Module docstring missing, or too late src/algebra/polynomial/big_operators.lean : line 9 : ERR_MOD : Module docstring missing, or too late @@ -161,19 +161,19 @@ src/analysis/analytic/basic.lean : line 755 : ERR_LIN : Line has more than 100 c 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 -src/analysis/analytic/composition.lean : line 905 : ERR_LIN : Line has more than 100 characters -src/analysis/analytic/composition.lean : line 906 : ERR_LIN : Line has more than 100 characters -src/analysis/analytic/composition.lean : line 909 : ERR_LIN : Line has more than 100 characters -src/analysis/analytic/composition.lean : line 949 : ERR_LIN : Line has more than 100 characters +src/analysis/analytic/composition.lean : line 900 : ERR_LIN : Line has more than 100 characters +src/analysis/analytic/composition.lean : line 901 : ERR_LIN : Line has more than 100 characters +src/analysis/analytic/composition.lean : line 904 : ERR_LIN : Line has more than 100 characters +src/analysis/analytic/composition.lean : line 944 : ERR_LIN : Line has more than 100 characters src/analysis/calculus/deriv.lean : line 1086 : ERR_LIN : Line has more than 100 characters src/analysis/calculus/deriv.lean : line 308 : ERR_LIN : Line has more than 100 characters -src/analysis/calculus/fderiv.lean : line 1927 : ERR_LIN : Line has more than 100 characters -src/analysis/calculus/fderiv.lean : line 205 : ERR_LIN : Line has more than 100 characters -src/analysis/calculus/fderiv.lean : line 2351 : ERR_LIN : Line has more than 100 characters -src/analysis/calculus/fderiv.lean : line 2520 : ERR_LIN : Line has more than 100 characters -src/analysis/calculus/fderiv.lean : line 307 : ERR_LIN : Line has more than 100 characters -src/analysis/calculus/fderiv.lean : line 404 : ERR_LIN : Line has more than 100 characters -src/analysis/calculus/fderiv.lean : line 974 : 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 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 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/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 @@ -239,10 +239,10 @@ src/analysis/normed_space/multilinear.lean : line 723 : ERR_LIN : Line has more src/analysis/normed_space/multilinear.lean : line 761 : ERR_LIN : Line has more than 100 characters src/analysis/normed_space/multilinear.lean : line 894 : ERR_LIN : Line has more than 100 characters src/analysis/normed_space/multilinear.lean : line 927 : ERR_LIN : Line has more than 100 characters -src/analysis/normed_space/operator_norm.lean : line 234 : 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 641 : ERR_LIN : Line has more than 100 characters -src/analysis/normed_space/operator_norm.lean : line 87 : 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 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 1357 : ERR_LIN : Line has more than 100 characters src/analysis/special_functions/pow.lean : line 295 : ERR_LIN : Line has more than 100 characters @@ -324,16 +324,14 @@ src/category_theory/epi_mono.lean : line 14 : ERR_MOD : Module docstring missing src/category_theory/eq_to_hom.lean : line 47 : ERR_LIN : Line has more than 100 characters src/category_theory/eq_to_hom.lean : line 50 : ERR_LIN : Line has more than 100 characters src/category_theory/eq_to_hom.lean : line 8 : ERR_MOD : Module docstring missing, or too late -src/category_theory/equivalence.lean : line 240 : ERR_LIN : Line has more than 100 characters -src/category_theory/equivalence.lean : line 245 : ERR_LIN : Line has more than 100 characters -src/category_theory/equivalence.lean : line 249 : ERR_LIN : Line has more than 100 characters -src/category_theory/equivalence.lean : line 261 : ERR_LIN : Line has more than 100 characters -src/category_theory/equivalence.lean : line 298 : ERR_LIN : Line has more than 100 characters -src/category_theory/equivalence.lean : line 547 : ERR_LIN : Line has more than 100 characters -src/category_theory/equivalence.lean : line 549 : ERR_LIN : Line has more than 100 characters -src/category_theory/equivalence.lean : line 56 : ERR_LIN : Line has more than 100 characters -src/category_theory/equivalence.lean : line 568 : ERR_LIN : Line has more than 100 characters -src/category_theory/equivalence.lean : line 571 : ERR_LIN : Line has more than 100 characters +src/category_theory/equivalence.lean : line 241 : ERR_LIN : Line has more than 100 characters +src/category_theory/equivalence.lean : line 246 : ERR_LIN : Line has more than 100 characters +src/category_theory/equivalence.lean : line 250 : ERR_LIN : Line has more than 100 characters +src/category_theory/equivalence.lean : line 262 : ERR_LIN : Line has more than 100 characters +src/category_theory/equivalence.lean : line 299 : ERR_LIN : Line has more than 100 characters +src/category_theory/equivalence.lean : line 525 : ERR_LIN : Line has more than 100 characters +src/category_theory/equivalence.lean : line 527 : ERR_LIN : Line has more than 100 characters +src/category_theory/equivalence.lean : line 57 : ERR_LIN : Line has more than 100 characters src/category_theory/filtered.lean : line 182 : ERR_LIN : Line has more than 100 characters src/category_theory/full_subcategory.lean : line 8 : ERR_MOD : Module docstring missing, or too late src/category_theory/fully_faithful.lean : line 9 : ERR_LIN : Line has more than 100 characters @@ -650,12 +648,12 @@ src/data/buffer/basic.lean : line 12 : ERR_MOD : Module docstring missing, or to src/data/char.lean : line 9 : ERR_MOD : Module docstring missing, or too late src/data/complex/basic.lean : line 108 : ERR_LIN : Line has more than 100 characters src/data/complex/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late -src/data/complex/exponential.lean : line 1177 : ERR_LIN : Line has more than 100 characters -src/data/complex/exponential.lean : line 1179 : ERR_LIN : Line has more than 100 characters -src/data/complex/exponential.lean : line 1225 : ERR_LIN : Line has more than 100 characters +src/data/complex/exponential.lean : line 1173 : ERR_LIN : Line has more than 100 characters +src/data/complex/exponential.lean : line 1175 : ERR_LIN : Line has more than 100 characters +src/data/complex/exponential.lean : line 1221 : ERR_LIN : Line has more than 100 characters src/data/complex/exponential.lean : line 166 : ERR_LIN : Line has more than 100 characters -src/data/complex/exponential.lean : line 549 : ERR_LIN : Line has more than 100 characters -src/data/complex/exponential.lean : line 856 : ERR_LIN : Line has more than 100 characters +src/data/complex/exponential.lean : line 545 : ERR_LIN : Line has more than 100 characters +src/data/complex/exponential.lean : line 852 : ERR_LIN : Line has more than 100 characters src/data/complex/is_R_or_C.lean : line 44 : ERR_LIN : Line has more than 100 characters src/data/complex/is_R_or_C.lean : line 616 : ERR_LIN : Line has more than 100 characters src/data/complex/is_R_or_C.lean : line 621 : ERR_LIN : Line has more than 100 characters @@ -799,7 +797,7 @@ src/data/mv_polynomial/variables.lean : line 31 : ERR_LIN : Line has more than 1 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/nat/basic.lean : line 103 : ERR_LIN : Line has more than 100 characters -src/data/nat/basic.lean : line 864 : ERR_LIN : Line has more than 100 characters +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 @@ -1138,8 +1136,8 @@ src/linear_algebra/linear_independent.lean : line 886 : ERR_LIN : Line has more src/linear_algebra/matrix.lean : line 711 : ERR_LIN : Line has more than 100 characters src/linear_algebra/matrix.lean : line 724 : ERR_LIN : Line has more than 100 characters src/linear_algebra/matrix.lean : line 865 : ERR_LIN : Line has more than 100 characters -src/linear_algebra/multilinear.lean : line 126 : ERR_LIN : Line has more than 100 characters -src/linear_algebra/multilinear.lean : line 524 : ERR_LIN : Line has more than 100 characters +src/linear_algebra/multilinear.lean : line 129 : ERR_LIN : Line has more than 100 characters +src/linear_algebra/multilinear.lean : line 527 : ERR_LIN : Line has more than 100 characters src/linear_algebra/multilinear.lean : line 63 : ERR_LIN : Line has more than 100 characters src/linear_algebra/multilinear.lean : line 78 : ERR_LIN : Line has more than 100 characters src/linear_algebra/special_linear_group.lean : line 53 : ERR_LIN : Line has more than 100 characters @@ -1394,13 +1392,11 @@ src/ring_theory/polynomial/basic.lean : line 701 : ERR_LIN : Line has more than src/ring_theory/polynomial/scale_roots.lean : line 10 : ERR_MOD : Module docstring missing, or too late src/ring_theory/polynomial/scale_roots.lean : line 89 : ERR_LIN : Line has more than 100 characters src/ring_theory/polynomial/scale_roots.lean : line 92 : ERR_LIN : Line has more than 100 characters -src/ring_theory/power_series.lean : line 189 : ERR_LIN : Line has more than 100 characters -src/ring_theory/power_series.lean : line 194 : ERR_LIN : Line has more than 100 characters -src/ring_theory/power_series.lean : line 690 : ERR_LIN : Line has more than 100 characters -src/ring_theory/power_series.lean : line 693 : ERR_LIN : Line has more than 100 characters +src/ring_theory/power_series.lean : line 679 : ERR_LIN : Line has more than 100 characters +src/ring_theory/power_series.lean : line 682 : ERR_LIN : Line has more than 100 characters src/ring_theory/principal_ideal_domain.lean : line 121 : ERR_LIN : Line has more than 100 characters src/ring_theory/principal_ideal_domain.lean : line 124 : ERR_LIN : Line has more than 100 characters -src/ring_theory/roots_of_unity.lean : line 149 : ERR_LIN : Line has more than 100 characters +src/ring_theory/roots_of_unity.lean : line 150 : ERR_LIN : Line has more than 100 characters src/ring_theory/subring.lean : line 408 : ERR_LIN : Line has more than 100 characters src/ring_theory/subring.lean : line 415 : ERR_LIN : Line has more than 100 characters src/ring_theory/subring.lean : line 459 : ERR_LIN : Line has more than 100 characters @@ -1807,8 +1803,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 498 : ERR_LIN : Line has more than 100 characters -src/topology/local_homeomorph.lean : line 509 : 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/metric_space/basic.lean : line 109 : ERR_LIN : Line has more than 100 characters src/topology/metric_space/basic.lean : line 1307 : ERR_LIN : Line has more than 100 characters src/topology/metric_space/basic.lean : line 15 : ERR_MOD : Module docstring missing, or too late