Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#6227)
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 Feb 14, 2021
1 parent 86e8a5d commit c54a8d0
Showing 1 changed file with 13 additions and 22 deletions.
35 changes: 13 additions & 22 deletions scripts/style-exceptions.txt
View file
Expand Up @@ -39,9 +39,9 @@ src/analysis/normed_space/operator_norm.lean : line 221 : ERR_LIN : Line has mor
src/analysis/normed_space/operator_norm.lean : line 34 : ERR_LIN : Line has more than 100 characters
src/analysis/normed_space/operator_norm.lean : line 91 : 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 295 : ERR_LIN : Line has more than 100 characters
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/pow.lean : line 301 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 302 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/pow.lean : line 554 : ERR_LIN : Line has more than 100 characters
src/analysis/special_functions/trigonometric.lean : line 1467 : ERR_LIN : Line has more than 100 characters
src/analysis/specific_limits.lean : line 213 : ERR_LIN : Line has more than 100 characters
src/analysis/specific_limits.lean : line 84 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -484,12 +484,6 @@ src/geometry/manifold/times_cont_mdiff.lean : line 990 : ERR_LIN : Line has more
src/group_theory/coset.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/group_theory/eckmann_hilton.lean : line 98 : ERR_LIN : Line has more than 100 characters
src/group_theory/free_abelian_group.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/group_theory/free_group.lean : line 129 : ERR_LIN : Line has more than 100 characters
src/group_theory/free_group.lean : line 176 : ERR_LIN : Line has more than 100 characters
src/group_theory/free_group.lean : line 18 : ERR_MOD : Module docstring missing, or too late
src/group_theory/free_group.lean : line 180 : ERR_LIN : Line has more than 100 characters
src/group_theory/free_group.lean : line 684 : ERR_LIN : Line has more than 100 characters
src/group_theory/free_group.lean : line 749 : ERR_LIN : Line has more than 100 characters
src/group_theory/presented_group.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/group_theory/presented_group.lean : line 51 : ERR_LIN : Line has more than 100 characters
src/group_theory/quotient_group.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -601,20 +595,18 @@ src/ring_theory/algebra_tower.lean : line 202 : ERR_LIN : Line has more than 100
src/ring_theory/algebra_tower.lean : line 77 : ERR_LIN : Line has more than 100 characters
src/ring_theory/dedekind_domain.lean : line 25 : ERR_LIN : Line has more than 100 characters
src/ring_theory/derivation.lean : line 205 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 109 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 112 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 187 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 200 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 215 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 219 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 259 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 261 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 263 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_ring.lean : line 83 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_ring.lean : line 86 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 190 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 203 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 218 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 222 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 262 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 264 : ERR_LIN : Line has more than 100 characters
src/ring_theory/free_comm_ring.lean : line 266 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/basic.lean : line 58 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 1311 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 1269 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 1272 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 140 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 1408 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 144 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 145 : ERR_LIN : Line has more than 100 characters
src/ring_theory/ideal/operations.lean : line 304 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -930,7 +922,6 @@ src/testing/slim_check/testable.lean : line 606 : ERR_LIN : Line has more than 1
src/testing/slim_check/testable.lean : line 741 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/floor_ring.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/group_completion.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/module.lean : line 1282 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/open_subgroup.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/ring.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/uniform_ring.lean : line 11 : ERR_MOD : Module docstring missing, or too late
Expand Down

0 comments on commit c54a8d0

Please sign in to comment.