Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#4564)
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 Oct 11, 2020
1 parent d8d6e18 commit 4dbebe3
Showing 1 changed file with 37 additions and 39 deletions.
76 changes: 37 additions & 39 deletions scripts/copy-mod-doc-exceptions.txt
View file
Expand Up @@ -331,10 +331,10 @@ src/analysis/normed_space/operator_norm.lean : line 736 : ERR_LIN : Line has mor
src/analysis/normed_space/operator_norm.lean : line 753 : 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/special_functions/arsinh.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/analysis/special_functions/pow.lean : line 1163 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 1186 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 304 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 305 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 528 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 551 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1040 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1053 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1059 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -762,12 +762,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 106 : 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 1031 : ERR_LIN : Line has more than 100 characters
src/data/complex/exponential.lean : line 1037 : ERR_LIN : Line has more than 100 characters
src/data/complex/exponential.lean : line 165 : ERR_LIN : Line has more than 100 characters
src/data/complex/exponential.lean : line 548 : ERR_LIN : Line has more than 100 characters
src/data/complex/exponential.lean : line 745 : ERR_LIN : Line has more than 100 characters
src/data/complex/exponential.lean : line 984 : ERR_LIN : Line has more than 100 characters
src/data/complex/exponential.lean : line 986 : ERR_LIN : Line has more than 100 characters
src/data/complex/exponential.lean : line 990 : ERR_LIN : Line has more than 100 characters
src/data/complex/exponential.lean : line 992 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 27 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 541 : ERR_LIN : Line has more than 100 characters
src/data/complex/is_R_or_C.lean : line 546 : ERR_LIN : Line has more than 100 characters
Expand All @@ -777,8 +777,8 @@ src/data/complex/is_R_or_C.lean : line 572 : ERR_LIN : Line has more than 100 ch
src/data/complex/is_R_or_C.lean : line 581 : ERR_LIN : Line has more than 100 characters
src/data/dlist/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/dlist/instances.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/data/equiv/basic.lean : line 1278 : ERR_LIN : Line has more than 100 characters
src/data/equiv/basic.lean : line 1389 : ERR_LIN : Line has more than 100 characters
src/data/equiv/basic.lean : line 1292 : ERR_LIN : Line has more than 100 characters
src/data/equiv/basic.lean : line 1403 : ERR_LIN : Line has more than 100 characters
src/data/equiv/basic.lean : line 51 : ERR_LIN : Line has more than 100 characters
src/data/equiv/basic.lean : line 771 : ERR_LIN : Line has more than 100 characters
src/data/equiv/denumerable.lean : line 14 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -1489,11 +1489,11 @@ src/order/conditionally_complete_lattice.lean : line 667 : ERR_LIN : Line has mo
src/order/conditionally_complete_lattice.lean : line 679 : ERR_LIN : Line has more than 100 characters
src/order/conditionally_complete_lattice.lean : line 810 : 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 233 : ERR_LIN : Line has more than 100 characters
src/order/filter/bases.lean : line 241 : ERR_LIN : Line has more than 100 characters
src/order/filter/bases.lean : line 36 : ERR_LIN : Line has more than 100 characters
src/order/filter/bases.lean : line 545 : ERR_LIN : Line has more than 100 characters
src/order/filter/bases.lean : line 82 : ERR_LIN : Line has more than 100 characters
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
src/order/filter/bases.lean : line 40 : ERR_LIN : Line has more than 100 characters
src/order/filter/bases.lean : line 563 : ERR_LIN : Line has more than 100 characters
src/order/filter/bases.lean : line 86 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1400 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 144 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1540 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -2131,8 +2131,8 @@ src/topology/algebra/uniform_group.lean : line 420 : ERR_LIN : Line has more tha
src/topology/algebra/uniform_ring.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/uniform_ring.lean : line 148 : ERR_LIN : Line has more than 100 characters
src/topology/bases.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/topology/bases.lean : line 157 : ERR_LIN : Line has more than 100 characters
src/topology/bases.lean : line 177 : ERR_LIN : Line has more than 100 characters
src/topology/bases.lean : line 162 : ERR_LIN : Line has more than 100 characters
src/topology/bases.lean : line 182 : ERR_LIN : Line has more than 100 characters
src/topology/bases.lean : line 45 : ERR_LIN : Line has more than 100 characters
src/topology/bases.lean : line 49 : ERR_LIN : Line has more than 100 characters
src/topology/bases.lean : line 68 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -2219,9 +2219,8 @@ src/topology/metric_space/closeds.lean : line 265 : ERR_LIN : Line has more than
src/topology/metric_space/emetric_space.lean : line 19 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/emetric_space.lean : line 318 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/emetric_space.lean : line 36 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/emetric_space.lean : line 696 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/emetric_space.lean : line 787 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/emetric_space.lean : line 797 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/emetric_space.lean : line 754 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/emetric_space.lean : line 764 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/emetric_space.lean : line 93 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/gluing.lean : line 106 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/gluing.lean : line 124 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -2361,34 +2360,33 @@ src/topology/subset_properties.lean : line 723 : ERR_LIN : Line has more than 10
src/topology/tactic.lean : line 84 : ERR_LIN : Line has more than 100 characters
src/topology/topological_fiber_bundle.lean : line 135 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/absolute_value.lean : line 71 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 1004 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 1116 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 1185 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 1198 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 1201 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 1298 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 1308 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 1313 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 1011 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 1123 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 1192 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 1205 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 1208 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 1305 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 1315 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 1320 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 1327 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 220 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 385 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 566 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 647 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 803 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 808 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 906 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 909 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 574 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 655 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 811 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 816 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 913 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/basic.lean : line 916 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/cauchy.lean : line 431 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/compact_separated.lean : line 129 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/completion.lean : line 150 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/completion.lean : line 175 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/completion.lean : line 256 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/completion.lean : line 293 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/completion.lean : line 416 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/completion.lean : line 456 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/completion.lean : line 467 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/completion.lean : line 523 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/completion.lean : line 528 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/completion.lean : line 257 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/completion.lean : line 294 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/completion.lean : line 417 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/completion.lean : line 457 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/completion.lean : line 468 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/completion.lean : line 524 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/completion.lean : line 529 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/separation.lean : line 125 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/separation.lean : line 284 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/separation.lean : line 314 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit 4dbebe3

Please sign in to comment.