Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-31 16:13 3ae893dc

View on Github →

fix(tactic/simps): do not reach unreachable code (#3637) Fixes #3636

Estimated changes

Modified src/tactic/simps.lean

Modified test/simps.lean

added structure needs_prop_class

added def test_prop_class