Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#6957)
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 Mar 30, 2021
1 parent b4ce9b7 commit 8d398a8
Showing 1 changed file with 1 addition and 53 deletions.
54 changes: 1 addition & 53 deletions scripts/style-exceptions.txt
View file
Expand Up @@ -95,9 +95,6 @@ src/data/pfunctor/multivariate/W.lean : line 42 : ERR_LIN : Line has more than 1
src/data/pnat/factors.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/pnat/intervals.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/pnat/xgcd.lean : line 25 : ERR_MOD : Module docstring missing, or too late
src/data/pnat/xgcd.lean : line 327 : ERR_LIN : Line has more than 100 characters
src/data/pnat/xgcd.lean : line 328 : ERR_LIN : Line has more than 100 characters
src/data/polynomial/iterated_deriv.lean : line 199 : ERR_LIN : Line has more than 100 characters
src/data/qpf/multivariate/basic.lean : line 7 : ERR_MOD : Module docstring missing, or too late
src/data/qpf/multivariate/basic.lean : line 74 : ERR_LIN : Line has more than 100 characters
src/data/qpf/multivariate/constructions/cofix.lean : line 38 : ERR_LIN : Line has more than 100 characters
Expand All @@ -120,7 +117,6 @@ src/data/sigma/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too
src/data/string/basic.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/data/string/defs.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/data/subtype.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/data/sym2.lean : line 173 : ERR_LIN : Line has more than 100 characters
src/data/sym2.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/ulift.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/data/zsqrtd/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
Expand All @@ -135,58 +131,25 @@ src/logic/relation.lean : line 10 : ERR_MOD : Module docstring missing, or too l
src/logic/relator.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/measure_theory/decomposition.lean : line 14 : ERR_MOD : Module docstring missing, or too late
src/meta/coinductive_predicates.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/meta/expr_lens.lean : line 130 : ERR_LIN : Line has more than 100 characters
src/meta/rb_map.lean : line 14 : ERR_LIN : Line has more than 100 characters
src/order/basic.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/order/boolean_algebra.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/order/bounded_lattice.lean : line 15 : ERR_MOD : Module docstring missing, or too late
src/order/complete_boolean_algebra.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/order/complete_lattice.lean : line 134 : ERR_LIN : Line has more than 100 characters
src/order/complete_lattice.lean : line 94 : ERR_LIN : Line has more than 100 characters
src/order/conditionally_complete_lattice.lean : line 526 : ERR_LIN : Line has more than 100 characters
src/order/conditionally_complete_lattice.lean : line 748 : ERR_LIN : Line has more than 100 characters
src/order/conditionally_complete_lattice.lean : line 760 : ERR_LIN : Line has more than 100 characters
src/order/conditionally_complete_lattice.lean : line 891 : ERR_LIN : Line has more than 100 characters
src/order/directed.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/order/filter/partial.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/order/fixed_points.lean : line 203 : ERR_LIN : Line has more than 100 characters
src/order/fixed_points.lean : line 207 : ERR_LIN : Line has more than 100 characters
src/order/lexicographic.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/order/lexicographic.lean : line 169 : ERR_LIN : Line has more than 100 characters
src/order/lexicographic.lean : line 172 : ERR_LIN : Line has more than 100 characters
src/order/lexicographic.lean : line 70 : ERR_LIN : Line has more than 100 characters
src/order/omega_complete_partial_order.lean : line 51 : ERR_LIN : Line has more than 100 characters
src/order/ord_continuous.lean : line 248 : ERR_LIN : Line has more than 100 characters
src/order/order_iso_nat.lean : line 12 : ERR_MOD : Module docstring missing, or too late
src/order/pilex.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/order/pilex.lean : line 92 : ERR_LIN : Line has more than 100 characters
src/order/preorder_hom.lean : line 124 : ERR_LIN : Line has more than 100 characters
src/order/preorder_hom.lean : line 131 : ERR_LIN : Line has more than 100 characters
src/order/rel_iso.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/order/zorn.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/set_theory/game/impartial.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/set_theory/game/nim.lean : line 83 : ERR_LIN : Line has more than 100 characters
src/set_theory/game/nim.lean : line 86 : ERR_LIN : Line has more than 100 characters
src/set_theory/game/nim.lean : line 91 : ERR_LIN : Line has more than 100 characters
src/set_theory/game/nim.lean : line 94 : ERR_LIN : Line has more than 100 characters
src/set_theory/lists.lean : line 13 : ERR_MOD : Module docstring missing, or too late
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
src/set_theory/zfc.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/system/random/basic.lean : line 130 : ERR_LIN : Line has more than 100 characters
src/system/random/basic.lean : line 287 : ERR_LIN : Line has more than 100 characters
src/system/random/basic.lean : line 290 : ERR_LIN : Line has more than 100 characters
src/tactic/abel.lean : line 276 : ERR_LIN : Line has more than 100 characters
src/tactic/algebra.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/apply_fun.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/auto_cases.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/cache.lean : line 87 : ERR_LIN : Line has more than 100 characters
src/tactic/chain.lean : line 13 : ERR_LIN : Line has more than 100 characters
src/tactic/chain.lean : line 32 : ERR_LIN : Line has more than 100 characters
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
Expand All @@ -200,13 +163,11 @@ src/tactic/delta_instance.lean : line 67 : ERR_LIN : Line has more than 100 char
src/tactic/delta_instance.lean : line 75 : ERR_LIN : Line has more than 100 characters
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/equiv_rw.lean : line 225 : ERR_LIN : Line has more than 100 characters
src/tactic/ext.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/tactic/fin_cases.lean : line 120 : ERR_LIN : Line has more than 100 characters
src/tactic/fin_cases.lean : line 121 : ERR_LIN : Line has more than 100 characters
src/tactic/fin_cases.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/tactic/find.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/tactic/generalizes.lean : line 118 : ERR_LIN : Line has more than 100 characters
src/tactic/hint.lean : line 57 : ERR_LIN : Line has more than 100 characters
src/tactic/hint.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/tactic/induction.lean : line 1252 : ERR_RNT : Reserved notation outside tactic.reserved_notation
src/tactic/interactive.lean : line 1057 : ERR_LIN : Line has more than 100 characters
Expand Down Expand Up @@ -360,23 +321,10 @@ src/topology/algebra/group_completion.lean : line 10 : ERR_MOD : Module docstrin
src/topology/algebra/open_subgroup.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/ring.lean : line 13 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/uniform_ring.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/topology/algebra/uniform_ring.lean : line 148 : ERR_LIN : Line has more than 100 characters
src/topology/bases.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/topology/basic.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/topology/category/Top/open_nhds.lean : line 9 : ERR_MOD : Module docstring missing, or too late
src/topology/homeomorph.lean : line 8 : ERR_MOD : Module docstring missing, or too late
src/topology/metric_space/basic.lean : line 22 : ERR_MOD : Module docstring missing, or too late
src/topology/metric_space/gromov_hausdorff.lean : line 62 : ERR_LIN : Line has more than 100 characters
src/topology/omega_complete_partial_order.lean : line 85 : ERR_LIN : Line has more than 100 characters
src/topology/separation.lean : line 11 : ERR_MOD : Module docstring missing, or too late
src/topology/sheaves/forget.lean : line 147 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf.lean : line 89 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf.lean : line 91 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf_condition/equalizer_products.lean : line 230 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/sheaf_condition/equalizer_products.lean : line 231 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/stalks.lean : line 10 : ERR_MOD : Module docstring missing, or too late
src/topology/sheaves/stalks.lean : line 127 : ERR_LIN : Line has more than 100 characters
src/topology/sheaves/stalks.lean : line 132 : ERR_LIN : Line has more than 100 characters
src/topology/subset_properties.lean : line 1113 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/absolute_value.lean : line 71 : ERR_LIN : Line has more than 100 characters
src/topology/uniform_space/compact_separated.lean : line 128 : ERR_LIN : Line has more than 100 characters

0 comments on commit 8d398a8

Please sign in to comment.