mathlib
782013db - fix(tactic/monotonicity): support monotone in mono (#3310)

Commit
5 years ago
fix(tactic/monotonicity): support monotone in mono (#3310) This PR allow the `mono` tactic to use lemmas stated using `monotone`. Mostly authored by Simon Hudon Co-authored-by: Simon Hudon <simon.hudon@gmail.com> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Author
Parents
Loading