Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#10391)
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 Nov 20, 2021
1 parent db926f0 commit bd6c6d5
Showing 1 changed file with 10 additions and 10 deletions.
20 changes: 10 additions & 10 deletions scripts/style-exceptions.txt
Expand Up @@ -5,9 +5,9 @@ src/category_theory/monad/adjunction.lean : line 9 : ERR_MOD : Module docstring
src/category_theory/monad/basic.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/computability/partrec_code.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/control/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/control/monad/cont.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/control/monad/cont.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/control/monad/writer.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/control/traversable/derive.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/control/traversable/derive.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/data/analysis/filter.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/analysis/topology.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/data/array/lemmas.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Expand All @@ -28,10 +28,10 @@ src/data/rbtree/init.lean : line 7 : ERR_MOD : Module docstring missing, or too
src/data/rbtree/insert.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/data/rbtree/main.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/data/rbtree/min_max.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/data/seq/computation.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/seq/computation.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/data/seq/parallel.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/data/seq/seq.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/seq/wseq.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/seq/wseq.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/deprecated/subfield.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/deprecated/subring.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/logic/relator.lean : line 11 : ERR_MOD : Module docstring missing, or too late
Expand All @@ -43,10 +43,10 @@ src/tactic/chain.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/converter/binders.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/tactic/converter/interactive.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/tactic/converter/old_conv.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/core.lean : line 18 : ERR_MOD : Module docstring missing, or too late
src/tactic/core.lean : line 15 : ERR_MOD : Module docstring missing, or too late
src/tactic/delta_instance.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/elide.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/ext.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/tactic/ext.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/find.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/hint.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/induction.lean : line 1328 : ERR_RNT : Reserved notation outside tactic.reserved_notation
Expand All @@ -55,10 +55,10 @@ src/tactic/lint/default.lean : line 11 : ERR_MOD : Module docstring missing, or
src/tactic/local_cache.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/monotonicity/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/monotonicity/interactive.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/tactic/monotonicity/lemmas.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/tactic/monotonicity/lemmas.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/tactic/noncomm_ring.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/nth_rewrite/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/nth_rewrite/congr.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/tactic/nth_rewrite/congr.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/omega/clause.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/tactic/omega/coeffs.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/tactic/omega/eq_elim.lean : line 7 : ERR_MOD : Module docstring missing, or too late
Expand All @@ -78,9 +78,9 @@ src/tactic/omega/nat/sub_elim.lean : line 7 : ERR_MOD : Module docstring missing
src/tactic/omega/prove_unsats.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/tactic/omega/term.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/tactic/push_neg.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/tactic/restate_axiom.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/restate_axiom.lean : line 8 : 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
src/tactic/rewrite_all/basic.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/show_term.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/simpa.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/slice.lean : line 8 : ERR_MOD : Module docstring missing, or too late
Expand Down

0 comments on commit bd6c6d5

Please sign in to comment.