Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-20 11:52 d001abfd

View on Github →

feat(tactic/basic): adds contrapose tactic (#1015)

  • feat(tactic/basic): adds contrapose tactic
  • fix(tactic/push_neg): fix is_prop testing
  • Setup error message testing following Rob, add tests for contrapose
  • refactor(tactic/interactive): move noninteractive success_if_fail_with_msg to tactic/core

Estimated changes

added theorem imp_of_not_imp_not