Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-08 17:46 55d430ca

View on Github →

feat(tactic/linter): add decidable_classical linter (#2352)

  • feat(tactic/linter): add decidable_classical linter
  • docstring
  • cleanup
  • fix build, cleanup
  • fix test
  • Update src/tactic/lint/type_classes.lean Co-Authored-By: Scott Morrison scott@tqft.net
  • Update src/tactic/lint/type_classes.lean Co-Authored-By: Scott Morrison scott@tqft.net
  • Update src/tactic/lint/default.lean Co-Authored-By: Scott Morrison scott@tqft.net
  • Update src/tactic/lint/type_classes.lean Co-Authored-By: Scott Morrison scott@tqft.net
  • Update src/data/dfinsupp.lean Co-Authored-By: Yury G. Kudryashov urkud@urkud.name

Estimated changes

modified theorem ceil_nonneg
modified theorem lt_nat_ceil
modified theorem nat_ceil_lt_add_one
modified theorem submodule.sum_mem
modified theorem decidable.eq_or_lt_of_le
modified theorem decidable.le_iff_lt_or_eq
modified theorem decidable.le_of_not_lt
modified theorem decidable.le_or_lt
modified theorem decidable.lt_or_eq_of_le
modified theorem decidable.lt_or_gt_of_ne
modified theorem decidable.lt_or_le
modified theorem decidable.lt_trichotomy
modified theorem decidable.ne_iff_lt_or_gt
modified theorem decidable.not_lt
modified theorem finset.prod_apply
modified theorem dfinsupp.map_range_def
modified theorem dfinsupp.subtype_domain_sum
modified theorem dfinsupp.support_zip_with
modified theorem dfinsupp.zip_with_def
modified theorem finset.card_eq_of_bijective
modified theorem finset.card_le_of_inj_on
modified theorem finset.disjoint_bind_left
modified theorem finset.disjoint_bind_right
modified theorem finset.fold_op_rel_iff_and
modified theorem finset.fold_op_rel_iff_or
modified theorem finset.singleton_bind
modified theorem finset.subset_image_iff
modified theorem finset.subset_union_elim
modified theorem hash_map.valid.modify
modified theorem int.exists_greatest_of_bdd
modified theorem int.exists_least_of_bdd
modified theorem pequiv.matrix_mul_apply
modified theorem pequiv.mul_matrix_apply
modified theorem pequiv.single_mul_single
modified def pequiv.to_matrix
modified theorem pequiv.to_matrix_bot
modified theorem pequiv.to_matrix_injective
modified theorem pequiv.to_matrix_refl
modified theorem pequiv.to_matrix_swap
modified theorem pequiv.to_matrix_symm
modified theorem pequiv.to_matrix_trans
modified theorem pequiv.to_pequiv_mul_matrix
modified theorem ennreal.sum_lt_top
modified theorem ennreal.sum_lt_top_iff
modified theorem ennreal.to_nnreal_sum
modified theorem ennreal.to_real_sum
modified theorem set.not_not_mem
modified theorem finite_field.card_units
modified theorem order_of_pos
modified theorem multilinear_map.sum_apply
modified theorem not_exists_not
modified theorem not_forall_not
modified theorem not_imp
modified theorem not_not
modified theorem algebra.adjoin_eq_range
modified theorem multiplicity.finset.prod
modified def associates.{u}
modified theorem imp_of_not_imp_not