chore(scripts): update nolints.txt (#8696)

I am happy to remove some nolints for you!
leanprover-community · Aug 16, 2021 · 69785fe · 69785fe
1 parent b97344c
commit 69785fe
Showing 1 changed file with 6 additions and 4 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -373,6 +373,12 @@ apply_nolint vector.to_array doc_blame
 apply_nolint vector.traverse doc_blame
 apply_nolint vector.traverse_def unused_arguments
 
+-- data/vector3.lean
+apply_nolint vector3 has_inhabited_instance
+apply_nolint vector3.cons_elim doc_blame
+apply_nolint vector3.nil_elim doc_blame
+apply_nolint vector3.rec_on doc_blame
+
 -- deprecated/subfield.lean
 apply_nolint is_subfield doc_blame
 
@@ -434,10 +440,6 @@ apply_nolint tactic.mono doc_blame
 
 -- number_theory/dioph.lean
 apply_nolint poly has_inhabited_instance
-apply_nolint vector3 has_inhabited_instance
-apply_nolint vector3.cons_elim doc_blame
-apply_nolint vector3.nil_elim doc_blame
-apply_nolint vector3.rec_on doc_blame
 
 -- number_theory/pell.lean
 apply_nolint pell.az unused_arguments