Commit 2022-09-02 10:43 880bf07d

feat(Mathlib/Tactic/PushNeg): implement the push_neg tactic (#344) This PR implements the push_neg tactic. This code is based on https://github.com/leanprover-community/mathlib4/pull/193/ and on the original Lean 3 push_neg code. It notably implements a new feature: if set_option push_neg.use_distrib true is set, then it performs (¬ (p ∧ q)) = (¬ p ∨ ¬ q) instead of (¬ (p ∧ q)) = (p → ¬ q). Note: I'm not too sure what the conventions are for options (i.e. is push_neg.use_distrib an appropriate name?). Also, I don't know what the "group" string of the option is for, so I left it blank.