Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-03 17:37 4ca1e634

View on Github →

chore(*): fix errors in library and sanity_check (#1499)

  • chore(*): some cleanup by sanity_check
  • fix(is_auto_generated): also check for ginductives
  • fix(sanity_check): imp_intro is sanity_skip
  • fix(sanity_check): don't report names of instances
  • first errors
  • second errors
  • doc(logic/basic): add note
  • add link to note
  • mention letI

Estimated changes

modified theorem finset.prod_eq_one
added theorem abs_add
deleted def abs_add
added theorem sub_abs_le_abs_sub
deleted def sub_abs_le_abs_sub
deleted def real.angle.angle
added def real.angle
modified def functor.const
deleted theorem turing.TM2to1.{l}
modified theorem finset.card_lt_card
modified theorem finset.fold_map
modified theorem finset.image_const
modified theorem finset.image_singleton
modified theorem finset.map_empty
modified def finset.pi.empty
modified theorem finset.subset_image_iff
modified theorem finset.subset_insert
deleted def opposite.opposite
added def opposite
added theorem computation.corec_eq
modified theorem finset.coe_to_finset'
added theorem Exists.imp
deleted def Exists.imp
modified theorem exists_imp_exists'
added def name.has_prefix
modified theorem principal_seg.equiv_lt_top
modified theorem principal_seg.lt_le_top
modified theorem principal_seg.top_eq
modified theorem tactic.interactive.{u}