Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
chore(scripts): update nolints.txt (#19065)
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 committed May 23, 2023
1 parent 38df578 commit cb9077f
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 22 deletions.
20 changes: 0 additions & 20 deletions scripts/nolints.txt
Original file line number Diff line number Diff line change
Expand Up @@ -179,10 +179,6 @@ apply_nolint list.sublists_aux doc_blame
apply_nolint list.sublists_aux₁ doc_blame
apply_nolint list.traverse doc_blame

-- data/matrix/basic.lean
apply_nolint matrix.mul_submatrix_one fintype_finite
apply_nolint matrix.one_submatrix_mul fintype_finite

-- data/matrix/basis.lean
apply_nolint matrix.induction_on fintype_finite
apply_nolint matrix.induction_on' fintype_finite
Expand Down Expand Up @@ -314,22 +310,6 @@ apply_nolint computation.parallel.aux1 doc_blame
apply_nolint computation.parallel.aux2 doc_blame
apply_nolint computation.parallel_rec doc_blame

-- data/seq/seq.lean
apply_nolint seq.bisim_o doc_blame
apply_nolint seq.corec.F doc_blame
apply_nolint seq.is_bisimulation doc_blame
apply_nolint seq.mem doc_blame

-- data/seq/wseq.lean
apply_nolint wseq.bisim_o doc_blame
apply_nolint wseq.destruct_append.aux doc_blame
apply_nolint wseq.destruct_join.aux doc_blame
apply_nolint wseq.drop.aux doc_blame
apply_nolint wseq.lift_rel_o doc_blame
apply_nolint wseq.mem doc_blame
apply_nolint wseq.tail.aux doc_blame
apply_nolint wseq.think_congr unused_arguments

-- data/stream/defs.lean
apply_nolint stream.corec doc_blame
apply_nolint stream.corec' doc_blame
Expand Down
4 changes: 2 additions & 2 deletions scripts/style-exceptions.txt
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,9 @@ src/control/monad/writer.lean : line 11 : ERR_MOD : Module docstring missing, or
src/control/traversable/derive.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/array/lemmas.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/bitvec/basic.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/buffer/basic.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/buffer/basic.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/data/qpf/multivariate/basic.lean : line 76 : ERR_LIN : Line has more than 100 characters
src/data/qpf/univariate/basic.lean : line 35 : ERR_LIN : Line has more than 100 characters
src/data/qpf/univariate/basic.lean : line 38 : ERR_LIN : Line has more than 100 characters
src/data/rbmap/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/rbmap/default.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/rbtree/basic.lean : line 10 : ERR_MOD : Module docstring missing, or too late
Expand Down

0 comments on commit cb9077f

Please sign in to comment.