Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5016)
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 Nov 17, 2020
1 parent 53f71f8 commit a2f3399
Showing 1 changed file with 46 additions and 46 deletions.
92 changes: 46 additions & 46 deletions scripts/copy-mod-doc-exceptions.txt
View file
Expand Up @@ -253,7 +253,7 @@ src/analysis/normed_space/operator_norm.lean : line 34 : ERR_LIN : Line has more
src/analysis/normed_space/operator_norm.lean : line 628 : 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 1242 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 1344 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 294 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 295 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 547 : ERR_LIN : Line has more than 100 characters
Expand All @@ -274,17 +274,17 @@ src/analysis/special_functions/trigonometric.lean : line 1363 : ERR_LIN : Line h
src/analysis/special_functions/trigonometric.lean : line 1366 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1380 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1390 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1452 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1503 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1553 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1625 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1808 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1889 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1892 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1999 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2002 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2102 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2146 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1451 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1502 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1552 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1624 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1807 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1888 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1891 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1998 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2001 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2101 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 2145 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 691 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 725 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 745 : ERR_LIN : Line has more than 100 characters
Expand All @@ -294,7 +294,7 @@ src/analysis/special_functions/trigonometric.lean : line 799 : ERR_LIN : Line ha
src/analysis/special_functions/trigonometric.lean : line 802 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 804 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 98 : ERR_LIN : Line has more than 100 characters
src/analysis/specific_limits.lean : line 584 : ERR_LIN : Line has more than 100 characters
src/analysis/specific_limits.lean : line 582 : 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
src/category_theory/abelian/non_preadditive.lean : line 191 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -884,9 +884,9 @@ src/data/padics/padic_norm.lean : line 126 : ERR_LIN : Line has more than 100 ch
src/data/padics/padic_norm.lean : line 139 : ERR_LIN : Line has more than 100 characters
src/data/padics/padic_norm.lean : line 150 : ERR_LIN : Line has more than 100 characters
src/data/padics/padic_norm.lean : line 162 : ERR_LIN : Line has more than 100 characters
src/data/padics/padic_norm.lean : line 345 : ERR_LIN : Line has more than 100 characters
src/data/padics/padic_norm.lean : line 343 : ERR_LIN : Line has more than 100 characters
src/data/padics/padic_norm.lean : line 366 : ERR_LIN : Line has more than 100 characters
src/data/padics/padic_norm.lean : line 368 : ERR_LIN : Line has more than 100 characters
src/data/padics/padic_norm.lean : line 370 : ERR_LIN : Line has more than 100 characters
src/data/padics/padic_numbers.lean : line 105 : ERR_LIN : Line has more than 100 characters
src/data/padics/padic_numbers.lean : line 14 : ERR_LIN : Line has more than 100 characters
src/data/padics/padic_numbers.lean : line 32 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1117,12 +1117,12 @@ src/group_theory/free_group.lean : line 180 : ERR_LIN : Line has more than 100 c
src/group_theory/free_group.lean : line 672 : ERR_LIN : Line has more than 100 characters
src/group_theory/free_group.lean : line 737 : ERR_LIN : Line has more than 100 characters
src/group_theory/order_of_element.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/group_theory/order_of_element.lean : line 373 : ERR_LIN : Line has more than 100 characters
src/group_theory/order_of_element.lean : line 413 : ERR_LIN : Line has more than 100 characters
src/group_theory/order_of_element.lean : line 423 : ERR_LIN : Line has more than 100 characters
src/group_theory/order_of_element.lean : line 453 : ERR_LIN : Line has more than 100 characters
src/group_theory/order_of_element.lean : line 371 : ERR_LIN : Line has more than 100 characters
src/group_theory/order_of_element.lean : line 411 : ERR_LIN : Line has more than 100 characters
src/group_theory/order_of_element.lean : line 421 : ERR_LIN : Line has more than 100 characters
src/group_theory/order_of_element.lean : line 451 : ERR_LIN : Line has more than 100 characters
src/group_theory/order_of_element.lean : line 496 : ERR_LIN : Line has more than 100 characters
src/group_theory/order_of_element.lean : line 498 : ERR_LIN : Line has more than 100 characters
src/group_theory/order_of_element.lean : line 500 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/cycles.lean : line 124 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/cycles.lean : line 127 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/cycles.lean : line 138 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1153,15 +1153,15 @@ src/group_theory/subgroup.lean : line 785 : ERR_LIN : Line has more than 100 cha
src/group_theory/subgroup.lean : line 820 : 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/basic.lean : line 1522 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 1554 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 1930 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2040 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2046 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2047 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2054 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2112 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2180 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 1520 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 1552 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 1928 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2038 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2044 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2045 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2052 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2110 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2178 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basis.lean : line 93 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/bilinear_form.lean : line 106 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/bilinear_form.lean : line 154 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1243,24 +1243,24 @@ src/number_theory/pell.lean : line 145 : ERR_LIN : Line has more than 100 charac
src/number_theory/pell.lean : line 149 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 168 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 196 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 312 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 351 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 353 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 357 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 311 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 350 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 352 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 356 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 368 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 369 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 370 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 381 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 390 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 427 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 437 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 443 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 454 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 460 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 463 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 467 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 471 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 473 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 487 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 380 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 389 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 426 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 436 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 442 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 453 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 459 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 462 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 466 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 470 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 472 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 486 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 68 : ERR_LIN : Line has more than 100 characters
src/number_theory/pell.lean : line 69 : ERR_LIN : Line has more than 100 characters
src/number_theory/primorial.lean : line 123 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit a2f3399

Please sign in to comment.