Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5790)
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 Jan 18, 2021
1 parent 2f824aa commit 3089b16
Showing 1 changed file with 9 additions and 29 deletions.
38 changes: 9 additions & 29 deletions scripts/style-exceptions.txt
View file
Expand Up @@ -685,8 +685,8 @@ src/data/set/disjointed.lean : line 10 : ERR_MOD : Module docstring missing, or
src/data/set/enumerate.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/data/set/function.lean : line 420 : ERR_LIN : Line has more than 100 characters
src/data/set/lattice.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/data/set/lattice.lean : line 466 : ERR_LIN : Line has more than 100 characters
src/data/set/lattice.lean : line 468 : ERR_LIN : Line has more than 100 characters
src/data/set/lattice.lean : line 470 : ERR_LIN : Line has more than 100 characters
src/data/set/lattice.lean : line 472 : ERR_LIN : Line has more than 100 characters
src/data/setoid/basic.lean : line 252 : ERR_LIN : Line has more than 100 characters
src/data/sigma/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/string/basic.lean : line 11 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -763,12 +763,12 @@ src/geometry/manifold/basic_smooth_bundle.lean : line 391 : ERR_LIN : Line has m
src/geometry/manifold/basic_smooth_bundle.lean : line 41 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/basic_smooth_bundle.lean : line 421 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/basic_smooth_bundle.lean : line 563 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/charted_space.lean : line 488 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/charted_space.lean : line 490 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/charted_space.lean : line 493 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/charted_space.lean : line 541 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/charted_space.lean : line 813 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/charted_space.lean : line 858 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/charted_space.lean : line 494 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/charted_space.lean : line 496 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/charted_space.lean : line 499 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/charted_space.lean : line 547 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/charted_space.lean : line 819 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/charted_space.lean : line 864 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/instances/real.lean : line 18 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/instances/real.lean : line 303 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/instances/real.lean : line 79 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -836,26 +836,6 @@ src/group_theory/order_of_element.lean : line 442 : ERR_LIN : Line has more than
src/group_theory/order_of_element.lean : line 472 : ERR_LIN : Line has more than 100 characters
src/group_theory/order_of_element.lean : line 517 : ERR_LIN : Line has more than 100 characters
src/group_theory/order_of_element.lean : line 519 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/cycles.lean : line 257 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/cycles.lean : line 260 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/cycles.lean : line 271 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/cycles.lean : line 30 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/cycles.lean : line 71 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/cycles.lean : line 78 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/cycles.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/group_theory/perm/cycles.lean : line 81 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/cycles.lean : line 84 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/cycles.lean : line 85 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/cycles.lean : line 86 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 117 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 124 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 127 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 130 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 160 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 257 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 286 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 468 : ERR_LIN : Line has more than 100 characters
src/group_theory/perm/sign.lean : line 51 : 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 @@ -1546,7 +1526,7 @@ src/topology/metric_space/gromov_hausdorff_realized.lean : line 234 : ERR_LIN :
src/topology/metric_space/gromov_hausdorff_realized.lean : line 404 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/gromov_hausdorff_realized.lean : line 75 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/gromov_hausdorff_realized.lean : line 77 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/isometry.lean : line 319 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/isometry.lean : line 356 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/lipschitz.lean : line 74 : ERR_LIN : Line has more than 100 characters
src/topology/metric_space/premetric_space.lean : line 82 : ERR_LIN : Line has more than 100 characters
src/topology/omega_complete_partial_order.lean : line 85 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit 3089b16

Please sign in to comment.