Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5892)
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 committed Jan 26, 2021
1 parent 5491c59 commit 01a7cde
Showing 1 changed file with 10 additions and 19 deletions.
29 changes: 10 additions & 19 deletions scripts/style-exceptions.txt
Original file line number Diff line number Diff line change
Expand Up @@ -7,16 +7,6 @@ archive/100-theorems-list/82_cubing_a_cube.lean : line 294 : ERR_LIN : Line has
archive/imo/imo1959_q1.lean : line 10 : ERR_MOD : Module docstring missing, or too late
archive/imo/imo1972_b2.lean : line 11 : ERR_MOD : Module docstring missing, or too late
archive/miu_language/basic.lean : line 53 : ERR_LIN : Line has more than 100 characters
archive/sensitivity.lean : line 406 : ERR_LIN : Line has more than 100 characters
archive/sensitivity.lean : line 409 : ERR_LIN : Line has more than 100 characters
archive/sensitivity.lean : line 410 : ERR_LIN : Line has more than 100 characters
archive/sensitivity.lean : line 411 : ERR_LIN : Line has more than 100 characters
archive/sensitivity.lean : line 412 : ERR_LIN : Line has more than 100 characters
archive/sensitivity.lean : line 413 : ERR_LIN : Line has more than 100 characters
archive/sensitivity.lean : line 414 : ERR_LIN : Line has more than 100 characters
archive/sensitivity.lean : line 415 : ERR_LIN : Line has more than 100 characters
archive/sensitivity.lean : line 416 : ERR_LIN : Line has more than 100 characters
archive/sensitivity.lean : line 420 : ERR_LIN : Line has more than 100 characters
src/algebra/algebra/subalgebra.lean : line 408 : ERR_LIN : Line has more than 100 characters
src/algebra/archimedean.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/algebra/category/Algebra/basic.lean : line 12 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -117,6 +107,7 @@ src/analysis/special_functions/pow.lean : line 295 : ERR_LIN : Line has more tha
src/analysis/special_functions/pow.lean : line 296 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 548 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1466 : ERR_LIN : Line has more than 100 characters
src/analysis/specific_limits.lean : line 210 : ERR_LIN : Line has more than 100 characters
src/analysis/specific_limits.lean : line 84 : 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
Expand Down Expand Up @@ -565,7 +556,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 624 : ERR_LIN : Line has more than 100 characters
src/data/nat/basic.lean : line 109 : ERR_LIN : Line has more than 100 characters
src/data/nat/basic.lean : line 851 : ERR_LIN : Line has more than 100 characters
src/data/nat/basic.lean : line 859 : 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/cast.lean : line 118 : ERR_LIN : Line has more than 100 characters
src/data/nat/dist.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -883,7 +874,7 @@ src/logic/relation.lean : line 10 : ERR_MOD : Module docstring missing, or too l
src/logic/relator.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/measure_theory/category/Meas.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/measure_theory/decomposition.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/measure_theory/measure_space.lean : line 1813 : ERR_LIN : Line has more than 100 characters
src/measure_theory/measure_space.lean : line 1830 : ERR_LIN : Line has more than 100 characters
src/measure_theory/measure_space.lean : line 65 : ERR_LIN : Line has more than 100 characters
src/meta/coinductive_predicates.lean : line 115 : ERR_LIN : Line has more than 100 characters
src/meta/coinductive_predicates.lean : line 12 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1415,13 +1406,13 @@ src/topology/algebra/group_completion.lean : line 84 : ERR_LIN : Line has more t
src/topology/algebra/group_completion.lean : line 90 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group_completion.lean : line 97 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group_completion.lean : line 99 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 1080 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 1090 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 300 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 522 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 554 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 608 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 675 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 1133 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 1143 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 353 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 575 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 607 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 661 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 728 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/multilinear.lean : line 185 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/multilinear.lean : line 245 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/multilinear.lean : line 46 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit 01a7cde

Please sign in to comment.