Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#4797)
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 Oct 27, 2020
1 parent 6e2980c commit 69db7a3
Showing 1 changed file with 19 additions and 31 deletions.
50 changes: 19 additions & 31 deletions scripts/copy-mod-doc-exceptions.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -174,10 +174,8 @@ src/algebra/lie/classical.lean : line 124 : ERR_LIN : Line has more than 100 cha
src/algebra/lie/classical.lean : line 215 : ERR_LIN : Line has more than 100 characters
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 114 : ERR_LIN : Line has more than 100 characters
src/algebra/module/basic.lean : line 259 : ERR_LIN : Line has more than 100 characters
src/algebra/module/basic.lean : line 412 : ERR_LIN : Line has more than 100 characters
src/algebra/module/basic.lean : line 528 : ERR_LIN : Line has more than 100 characters
src/algebra/module/basic.lean : line 112 : ERR_LIN : Line has more than 100 characters
src/algebra/module/basic.lean : line 309 : ERR_LIN : Line has more than 100 characters
src/algebra/module/ordered.lean : line 158 : ERR_LIN : Line has more than 100 characters
src/algebra/module/pi.lean : line 63 : ERR_LIN : Line has more than 100 characters
src/algebra/module/pi.lean : line 77 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -884,8 +882,8 @@ src/data/multiset/nodup.lean : line 92 : ERR_LIN : Line has more than 100 charac
src/data/multiset/range.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/mv_polynomial/basic.lean : line 107 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/basic.lean : line 159 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/basic.lean : line 509 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/basic.lean : line 814 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/basic.lean : line 510 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/basic.lean : line 815 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/comm_ring.lean : line 113 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/counit.lean : line 19 : ERR_LIN : Line has more than 100 characters
src/data/mv_polynomial/equiv.lean : line 104 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -982,8 +980,8 @@ src/data/pnat/xgcd.lean : line 24 : ERR_MOD : Module docstring missing, or too l
src/data/pnat/xgcd.lean : line 328 : ERR_LIN : Line has more than 100 characters
src/data/pnat/xgcd.lean : line 329 : ERR_LIN : Line has more than 100 characters
src/data/polynomial/algebra_map.lean : line 53 : ERR_LIN : Line has more than 100 characters
src/data/polynomial/degree/basic.lean : line 327 : ERR_LIN : Line has more than 100 characters
src/data/polynomial/degree/basic.lean : line 468 : ERR_LIN : Line has more than 100 characters
src/data/polynomial/degree/basic.lean : line 336 : ERR_LIN : Line has more than 100 characters
src/data/polynomial/degree/basic.lean : line 477 : ERR_LIN : Line has more than 100 characters
src/data/polynomial/degree/trailing_degree.lean : line 104 : ERR_LIN : Line has more than 100 characters
src/data/polynomial/degree/trailing_degree.lean : line 119 : ERR_LIN : Line has more than 100 characters
src/data/polynomial/degree/trailing_degree.lean : line 132 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1256,15 +1254,15 @@ src/linear_algebra/affine_space/basic.lean : line 10 : ERR_MOD : Module docstrin
src/linear_algebra/affine_space/combination.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/linear_algebra/affine_space/finite_dimensional.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/linear_algebra/affine_space/independent.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/linear_algebra/basic.lean : line 1493 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 1525 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2040 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2150 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2156 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2157 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2164 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2222 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2290 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 1485 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 1517 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 1893 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2003 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2009 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2010 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2017 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2075 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2143 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basis.lean : line 93 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/bilinear_form.lean : line 106 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/bilinear_form.lean : line 154 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1785,7 +1783,7 @@ src/tactic/push_neg.lean : line 180 : ERR_LIN : Line has more than 100 character
src/tactic/push_neg.lean : line 181 : ERR_LIN : Line has more than 100 characters
src/tactic/push_neg.lean : line 183 : ERR_LIN : Line has more than 100 characters
src/tactic/push_neg.lean : line 184 : ERR_LIN : Line has more than 100 characters
src/tactic/rcases.lean : line 704 : ERR_LIN : Line has more than 100 characters
src/tactic/rcases.lean : line 741 : ERR_LIN : Line has more than 100 characters
src/tactic/restate_axiom.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/rewrite.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/rewrite_all/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Expand All @@ -1799,19 +1797,9 @@ src/tactic/simp_result.lean : line 94 : ERR_LIN : Line has more than 100 charact
src/tactic/simp_rw.lean : line 44 : ERR_LIN : Line has more than 100 characters
src/tactic/simpa.lean : line 38 : ERR_LIN : Line has more than 100 characters
src/tactic/simpa.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/simps.lean : line 115 : ERR_LIN : Line has more than 100 characters
src/tactic/simps.lean : line 126 : ERR_LIN : Line has more than 100 characters
src/tactic/simps.lean : line 129 : ERR_LIN : Line has more than 100 characters
src/tactic/simps.lean : line 146 : ERR_LIN : Line has more than 100 characters
src/tactic/simps.lean : line 159 : ERR_LIN : Line has more than 100 characters
src/tactic/simps.lean : line 161 : ERR_LIN : Line has more than 100 characters
src/tactic/simps.lean : line 17 : ERR_LIN : Line has more than 100 characters
src/tactic/simps.lean : line 225 : ERR_LIN : Line has more than 100 characters
src/tactic/simps.lean : line 259 : ERR_LIN : Line has more than 100 characters
src/tactic/simps.lean : line 335 : ERR_LIN : Line has more than 100 characters
src/tactic/simps.lean : line 337 : ERR_LIN : Line has more than 100 characters
src/tactic/simps.lean : line 345 : ERR_LIN : Line has more than 100 characters
src/tactic/simps.lean : line 353 : ERR_LIN : Line has more than 100 characters
src/tactic/simps.lean : line 240 : ERR_LIN : Line has more than 100 characters
src/tactic/simps.lean : line 366 : ERR_LIN : Line has more than 100 characters
src/tactic/simps.lean : line 374 : ERR_LIN : Line has more than 100 characters
src/tactic/slice.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/slim_check.lean : line 186 : ERR_LIN : Line has more than 100 characters
src/tactic/slim_check.lean : line 188 : ERR_LIN : Line has more than 100 characters
Expand Down

0 comments on commit 69db7a3

Please sign in to comment.