Commit 2020-07-08 20:57 782013db

View on Github →

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

Estimated changes

Modified scripts/nolints.txt

Modified src/tactic/monotonicity/basic.lean

Modified src/tactic/monotonicity/interactive.lean

Modified test/monotonicity/test_cases.lean

added theorem test