Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#2517)
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 Apr 25, 2020
1 parent 22d89c4 commit 06f8c55
Showing 1 changed file with 0 additions and 12 deletions.
12 changes: 0 additions & 12 deletions scripts/nolints.txt
Expand Up @@ -1681,15 +1681,6 @@ apply_nolint vector.to_array doc_blame
apply_nolint vector.traverse doc_blame
apply_nolint vector.traverse_def unused_arguments

-- data/zmod/basic.lean
apply_nolint zmod doc_blame
apply_nolint zmod.cast doc_blame
apply_nolint zmod.units_equiv_coprime doc_blame
apply_nolint zmodp doc_blame

-- data/zmod/quadratic_reciprocity.lean
apply_nolint zmodp.legendre_sym doc_blame

-- data/zsqrtd/basic.lean
apply_nolint zsqrtd.le doc_blame
apply_nolint zsqrtd.lt doc_blame
Expand Down Expand Up @@ -1863,9 +1854,6 @@ apply_nolint simple_group doc_blame

-- group_theory/sylow.lean
apply_nolint sylow.fixed_points_mul_left_cosets_equiv_quotient doc_blame
apply_nolint sylow.mk_vector_prod_eq_one doc_blame
apply_nolint sylow.rotate_vectors_prod_eq_one doc_blame
apply_nolint sylow.vectors_prod_eq_one doc_blame

-- linear_algebra/basic.lean
apply_nolint linear_equiv.to_equiv doc_blame
Expand Down

0 comments on commit 06f8c55

Please sign in to comment.