Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5272)
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 8, 2020
1 parent b173925 commit 35f0862
Showing 1 changed file with 20 additions and 24 deletions.
44 changes: 20 additions & 24 deletions scripts/copy-mod-doc-exceptions.txt
View file
Expand Up @@ -159,10 +159,10 @@ 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 907 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 910 : ERR_LIN : Line has more than 100 characters
src/analysis/analytic/composition.lean : line 950 : 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/calculus/deriv.lean : line 1095 : 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 1865 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -690,9 +690,6 @@ src/data/equiv/mul_add.lean : line 493 : ERR_LIN : Line has more than 100 charac
src/data/equiv/mul_add.lean : line 506 : ERR_LIN : Line has more than 100 characters
src/data/equiv/nat.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/data/erased.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/fin.lean : line 1072 : ERR_LIN : Line has more than 100 characters
src/data/fin.lean : line 290 : ERR_LIN : Line has more than 100 characters
src/data/fin.lean : line 386 : ERR_LIN : Line has more than 100 characters
src/data/fin2.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/data/finset/gcd.lean : line 133 : ERR_LIN : Line has more than 100 characters
src/data/finsupp/pointwise.lean : line 57 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -922,7 +919,7 @@ src/data/seq/computation.lean : line 11 : ERR_MOD : Module docstring missing, or
src/data/seq/parallel.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/data/seq/seq.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/seq/wseq.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/set/basic.lean : line 2302 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 2311 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 469 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 554 : ERR_LIN : Line has more than 100 characters
src/data/set/basic.lean : line 658 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -978,7 +975,7 @@ src/deprecated/subgroup.lean : line 675 : ERR_LIN : Line has more than 100 chara
src/deprecated/subring.lean : line 133 : ERR_LIN : Line has more than 100 characters
src/deprecated/subring.lean : line 15 : ERR_LIN : Line has more than 100 characters
src/deprecated/subring.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/dynamics/circle/rotation_number/translation_number.lean : line 156 : ERR_LIN : Line has more than 100 characters
src/dynamics/circle/rotation_number/translation_number.lean : line 264 : ERR_LIN : Line has more than 100 characters
src/field_theory/algebraic_closure.lean : line 239 : ERR_LIN : Line has more than 100 characters
src/field_theory/algebraic_closure.lean : line 66 : ERR_LIN : Line has more than 100 characters
src/field_theory/algebraic_closure.lean : line 91 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1171,9 +1168,9 @@ src/linear_algebra/multilinear.lean : line 509 : ERR_LIN : Line has more than 10
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
src/logic/basic.lean : line 491 : ERR_LIN : Line has more than 100 characters
src/logic/basic.lean : line 568 : ERR_LIN : Line has more than 100 characters
src/logic/basic.lean : line 868 : ERR_LIN : Line has more than 100 characters
src/logic/basic.lean : line 494 : ERR_LIN : Line has more than 100 characters
src/logic/basic.lean : line 571 : ERR_LIN : Line has more than 100 characters
src/logic/basic.lean : line 871 : ERR_LIN : Line has more than 100 characters
src/logic/function/basic.lean : line 322 : ERR_LIN : Line has more than 100 characters
src/logic/function/basic.lean : line 496 : ERR_LIN : Line has more than 100 characters
src/logic/function/basic.lean : line 536 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1267,15 +1264,15 @@ src/order/filter/bases.lean : line 259 : ERR_LIN : Line has more than 100 charac
src/order/filter/bases.lean : line 40 : ERR_LIN : Line has more than 100 characters
src/order/filter/bases.lean : line 625 : 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 1324 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1464 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1327 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1467 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 147 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1470 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1487 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1767 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1919 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 2047 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 2287 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1473 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1490 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1770 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 1922 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 2050 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 2290 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 657 : ERR_LIN : Line has more than 100 characters
src/order/filter/basic.lean : line 667 : ERR_LIN : Line has more than 100 characters
src/order/filter/extr.lean : line 301 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1787,7 +1784,7 @@ src/topology/algebra/group_completion.lean : line 69 : ERR_LIN : Line has more t
src/topology/algebra/group_completion.lean : line 75 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group_completion.lean : line 82 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group_completion.lean : line 84 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/infinite_sum.lean : line 678 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/infinite_sum.lean : line 697 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 1078 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 1088 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 300 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -2054,7 +2051,6 @@ src/topology/uniform_space/separation.lean : line 429 : ERR_LIN : Line has more
src/topology/uniform_space/separation.lean : line 431 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/separation.lean : line 46 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/uniform_convergence.lean : line 320 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/uniform_embedding.lean : line 347 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/uniform_embedding.lean : line 394 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/uniform_embedding.lean : line 401 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/uniform_embedding.lean : line 89 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/uniform_embedding.lean : line 348 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/uniform_embedding.lean : line 395 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/uniform_embedding.lean : line 402 : ERR_LIN : Line has more than 100 characters

0 comments on commit 35f0862

Please sign in to comment.