Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5673)
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 9, 2021
1 parent 1294500 commit faf1a98
Showing 1 changed file with 18 additions and 18 deletions.
36 changes: 18 additions & 18 deletions scripts/style-exceptions.txt
View file
Expand Up @@ -105,7 +105,6 @@ src/algebra/lie/classical.lean : line 215 : ERR_LIN : Line has more than 100 cha
src/algebra/lie/classical.lean : line 363 : ERR_LIN : Line has more than 100 characters
src/algebra/linear_recurrence.lean : line 172 : ERR_LIN : Line has more than 100 characters
src/algebra/module/basic.lean : line 117 : ERR_LIN : Line has more than 100 characters
src/algebra/module/basic.lean : line 340 : ERR_LIN : Line has more than 100 characters
src/algebra/module/ordered.lean : line 182 : ERR_LIN : Line has more than 100 characters
src/algebra/module/ordered.lean : line 190 : ERR_LIN : Line has more than 100 characters
src/algebra/module/ordered.lean : line 193 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -759,8 +758,8 @@ src/data/mv_polynomial/variables.lean : line 28 : ERR_LIN : Line has more than 1
src/data/mv_polynomial/variables.lean : line 31 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/variables.lean : line 34 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/variables.lean : line 621 : ERR_LIN : Line has more than 100 characters
src/data/nat/basic.lean : line 103 : ERR_LIN : Line has more than 100 characters
src/data/nat/basic.lean : line 867 : 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 870 : ERR_LIN : Line has more than 100 characters
src/data/nat/cast.lean : line 101 : 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/dist.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Expand Down Expand Up @@ -1002,18 +1001,18 @@ src/geometry/manifold/mfderiv.lean : line 652 : ERR_LIN : Line has more than 100
src/geometry/manifold/mfderiv.lean : line 713 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/mfderiv.lean : line 786 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/smooth_manifold_with_corners.lean : line 170 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 1280 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 1540 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 1370 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 1630 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 244 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 255 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 266 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 277 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 293 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 331 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 398 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 497 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 523 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 900 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 294 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 305 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 341 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 401 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 468 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 567 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 593 : ERR_LIN : Line has more than 100 characters
src/geometry/manifold/times_cont_mdiff.lean : line 990 : ERR_LIN : Line has more than 100 characters
src/group_theory/abelianization.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/group_theory/archimedean.lean : line 43 : ERR_LIN : Line has more than 100 characters
src/group_theory/coset.lean : line 259 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1375,12 +1374,12 @@ src/ring_theory/witt_vector/witt_polynomial.lean : line 13 : ERR_MOD : Module do
src/ring_theory/witt_vector/witt_polynomial.lean : line 137 : ERR_LIN : Line has more than 100 characters
src/ring_theory/witt_vector/witt_polynomial.lean : line 232 : ERR_LIN : Line has more than 100 characters
src/ring_theory/witt_vector/witt_polynomial.lean : line 283 : ERR_LIN : Line has more than 100 characters
src/set_theory/cardinal.lean : line 1032 : ERR_LIN : Line has more than 100 characters
src/set_theory/cardinal.lean : line 1036 : ERR_LIN : Line has more than 100 characters
src/set_theory/cardinal.lean : line 1026 : ERR_LIN : Line has more than 100 characters
src/set_theory/cardinal.lean : line 1030 : ERR_LIN : Line has more than 100 characters
src/set_theory/cardinal.lean : line 104 : ERR_LIN : Line has more than 100 characters
src/set_theory/cardinal.lean : line 470 : ERR_LIN : Line has more than 100 characters
src/set_theory/cardinal.lean : line 862 : ERR_LIN : Line has more than 100 characters
src/set_theory/cardinal_ordinal.lean : line 253 : ERR_LIN : Line has more than 100 characters
src/set_theory/cardinal.lean : line 462 : ERR_LIN : Line has more than 100 characters
src/set_theory/cardinal.lean : line 856 : ERR_LIN : Line has more than 100 characters
src/set_theory/cardinal_ordinal.lean : line 254 : ERR_LIN : Line has more than 100 characters
src/set_theory/cofinality.lean : line 343 : ERR_LIN : Line has more than 100 characters
src/set_theory/cofinality.lean : line 359 : ERR_LIN : Line has more than 100 characters
src/set_theory/game/impartial.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Expand All @@ -1392,6 +1391,7 @@ src/set_theory/lists.lean : line 13 : ERR_MOD : Module docstring missing, or too
src/set_theory/ordinal.lean : line 1131 : ERR_LIN : Line has more than 100 characters
src/set_theory/ordinal_arithmetic.lean : line 1271 : ERR_LIN : Line has more than 100 characters
src/set_theory/ordinal_arithmetic.lean : line 1578 : ERR_LIN : Line has more than 100 characters
src/set_theory/ordinal_arithmetic.lean : line 756 : ERR_LIN : Line has more than 100 characters
src/set_theory/schroeder_bernstein.lean : line 103 : ERR_LIN : Line has more than 100 characters
src/set_theory/schroeder_bernstein.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/set_theory/surreal.lean : line 366 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit faf1a98

Please sign in to comment.