From 01a7cde647bd8d6f7e1b4c10373d7413cefa2455 Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Tue, 26 Jan 2021 01:48:59 +0000 Subject: [PATCH] chore(scripts): update nolints.txt (#5892) I am happy to remove some nolints for you! --- scripts/style-exceptions.txt | 29 ++++++++++------------------- 1 file changed, 10 insertions(+), 19 deletions(-) diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt index 13c1b1ab0a47d..678f7107b0d14 100644 --- a/scripts/style-exceptions.txt +++ b/scripts/style-exceptions.txt @@ -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 @@ -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 @@ -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 @@ -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 @@ -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