Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5441)
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 20, 2020
1 parent 1cb9727 commit a9fb069
Showing 1 changed file with 37 additions and 41 deletions.
78 changes: 37 additions & 41 deletions scripts/copy-mod-doc-exceptions.txt
View file
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit a9fb069

Please sign in to comment.