diff --git a/scripts/nolints.txt b/scripts/nolints.txt index 1bc4ed2a390df..377fdb1aaee1c 100644 --- 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