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.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
added theorem Exists.imp
deleted def Exists.imp
modified theorem exists_imp_exists'