Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#16384)
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 Sep 5, 2022
1 parent e1d2f5b commit 9b11656
Showing 1 changed file with 0 additions and 70 deletions.
70 changes: 0 additions & 70 deletions scripts/nolints.txt
Expand Up @@ -423,82 +423,16 @@ apply_nolint subgroup.card_subgroup_dvd_card to_additive_doc
-- group_theory/group_action/sub_mul_action.lean
apply_nolint sub_mul_action.has_zero fails_quickly

-- linear_algebra/affine_space/affine_subspace.lean
apply_nolint affine_span.nonempty fails_quickly
apply_nolint affine_subspace.to_add_torsor fails_quickly

-- linear_algebra/affine_space/basis.lean
apply_nolint affine_basis.affine_independent_of_to_matrix_right_inv fintype_finite
apply_nolint affine_basis.affine_span_eq_top_of_to_matrix_left_inv fintype_finite
apply_nolint affine_basis.ext_elem fintype_finite

-- linear_algebra/affine_space/finite_dimensional.lean
apply_nolint finite_dimensional_direction_affine_span_image_of_fintype fintype_finite
apply_nolint finite_dimensional_direction_affine_span_of_fintype fintype_finite
apply_nolint finite_dimensional_vector_span_image_of_fintype fintype_finite
apply_nolint finite_dimensional_vector_span_of_fintype fintype_finite

-- linear_algebra/alternating.lean
apply_nolint basis.ext_alternating fintype_finite

-- linear_algebra/determinant.lean
apply_nolint alternating_map.map_basis_eq_zero_iff fintype_finite
apply_nolint alternating_map.map_basis_ne_zero_iff fintype_finite
apply_nolint linear_map.det_zero' fintype_finite

-- linear_algebra/dimension.lean
apply_nolint dim_pi fintype_finite

-- linear_algebra/dual.lean
apply_nolint basis.dual_dim_eq fintype_finite
apply_nolint basis.eval_range fintype_finite
apply_nolint basis.to_dual_range fintype_finite
apply_nolint basis.total_coord fintype_finite

-- linear_algebra/finsupp_vector_space.lean
apply_nolint cardinal_lt_aleph_0_of_finite_dimensional fintype_finite

-- linear_algebra/free_module/finite/basic.lean
apply_nolint module.finite.matrix fintype_finite
apply_nolint module.finite.of_basis fintype_finite

-- linear_algebra/free_module/pid.lean
apply_nolint ideal.exists_smith_normal_form fintype_finite
apply_nolint submodule.basis_of_pid_aux fintype_finite
apply_nolint submodule.exists_smith_normal_form_of_le fintype_finite
apply_nolint submodule.nonempty_basis_of_pid fintype_finite

-- linear_algebra/free_module/rank.lean
apply_nolint module.free.rank_matrix fintype_finite
apply_nolint module.free.rank_matrix' fintype_finite
apply_nolint module.free.rank_matrix'' fintype_finite
apply_nolint module.free.rank_pi_fintype fintype_finite

-- linear_algebra/matrix/finite_dimensional.lean
apply_nolint matrix.finite_dimensional fintype_finite

-- linear_algebra/matrix/reindex.lean
apply_nolint matrix.mul_reindex_linear_equiv_one fintype_finite

-- linear_algebra/matrix/transvection.lean
apply_nolint matrix.update_row_eq_transvection fintype_finite

-- linear_algebra/multilinear/basis.lean
apply_nolint basis.ext_multilinear fintype_finite

-- linear_algebra/multilinear/finite_dimensional.lean
apply_nolint module.finite.multilinear_map fintype_finite
apply_nolint module.free.multilinear_map fintype_finite

-- linear_algebra/orientation.lean
apply_nolint basis.map_orientation_eq_det_inv_smul fintype_finite

-- linear_algebra/std_basis.lean
apply_nolint linear_map.supr_range_std_basis fintype_finite

-- linear_algebra/trace.lean
apply_nolint linear_map.trace_eq_contract_of_basis fintype_finite

-- logic/relator.lean
apply_nolint relator.bi_total doc_blame
apply_nolint relator.bi_unique doc_blame
Expand Down Expand Up @@ -533,10 +467,6 @@ apply_nolint tactic.coinductive_predicate doc_blame
apply_nolint tactic.interactive.coinduction doc_blame
apply_nolint tactic.mono doc_blame

-- model_theory/definability.lean
apply_nolint set.definable.image_comp fintype_finite
apply_nolint set.definable.image_comp_embedding fintype_finite

-- model_theory/direct_limit.lean
apply_nolint first_order.language.direct_limit.exists_quotient_mk_sigma_mk_eq fintype_finite
apply_nolint first_order.language.direct_limit.exists_unify_eq fintype_finite
Expand Down

0 comments on commit 9b11656

Please sign in to comment.