Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#5250)
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 Dec 6, 2020
1 parent 7e8e174 commit 065bd5f
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 22 deletions.
42 changes: 21 additions & 21 deletions scripts/copy-mod-doc-exceptions.txt
View file
Expand Up @@ -763,26 +763,26 @@ src/data/matrix/pequiv.lean : line 137 : ERR_LIN : Line has more than 100 charac
src/data/matrix/pequiv.lean : line 143 : ERR_LIN : Line has more than 100 characters
src/data/matrix/pequiv.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/mllist.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/data/multiset/basic.lean : line 1035 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1036 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 116 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 128 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1289 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1290 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 133 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1727 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1736 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1752 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1755 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 1944 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 2063 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 542 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 666 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 677 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 684 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 704 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 707 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 719 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 722 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 972 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 543 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 667 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 678 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 685 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 705 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 708 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 720 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 723 : ERR_LIN : Line has more than 100 characters
src/data/multiset/basic.lean : line 973 : ERR_LIN : Line has more than 100 characters
src/data/multiset/fold.lean : line 25 : ERR_LIN : Line has more than 100 characters
src/data/multiset/fold.lean : line 32 : ERR_LIN : Line has more than 100 characters
src/data/multiset/fold.lean : line 49 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1130,15 +1130,15 @@ src/group_theory/subgroup.lean : line 803 : ERR_LIN : Line has more than 100 cha
src/group_theory/subgroup.lean : line 838 : ERR_LIN : Line has more than 100 characters
src/group_theory/submonoid/operations.lean : line 560 : ERR_LIN : Line has more than 100 characters
src/group_theory/sylow.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/linear_algebra/basic.lean : line 1522 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 1554 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 1930 : 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 2046 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2047 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2054 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2112 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2180 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 1520 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 1552 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 1928 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2038 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2044 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2045 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2052 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2110 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/basic.lean : line 2178 : 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/char_poly/coeff.lean : line 190 : ERR_LIN : Line has more than 100 characters
src/linear_algebra/char_poly/coeff.lean : line 24 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -1787,7 +1787,7 @@ src/topology/algebra/group_completion.lean : line 69 : ERR_LIN : Line has more t
src/topology/algebra/group_completion.lean : line 75 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group_completion.lean : line 82 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/group_completion.lean : line 84 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/infinite_sum.lean : line 675 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/infinite_sum.lean : line 678 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 1078 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 1088 : ERR_LIN : Line has more than 100 characters
src/topology/algebra/module.lean : line 300 : ERR_LIN : Line has more than 100 characters
Expand Down
1 change: 0 additions & 1 deletion scripts/nolints.txt
View file
Expand Up @@ -317,7 +317,6 @@ apply_nolint tactic.mllist.take doc_blame unused_arguments
apply_nolint tactic.mllist.uncons doc_blame unused_arguments

-- data/multiset/basic.lean
apply_nolint multiset.choose doc_blame
apply_nolint multiset.decidable_exists_multiset doc_blame
apply_nolint multiset.decidable_forall_multiset doc_blame
apply_nolint multiset.rec_on doc_blame
Expand Down

0 comments on commit 065bd5f

Please sign in to comment.