Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-21 08:06 4082136e

View on Github →

feat(tactic/refine_struct): match { .. } in subexpressions (#162)

Estimated changes

Modified tactic/interactive.lean

Modified tests/tactics.lean

added def my_bar

added def my_foo