Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-08 06:57 732ec0ef

View on Github →

feat(tactic/rcases): rcases_hint, rintro_hint

Estimated changes

Modified docs/tactics.md

Modified tactic/basic.lean

Modified tactic/interactive.lean

added structure tactic.interactive.rcases_config

deleted def tactic.interactive.rcases_patt_inverted

Modified tactic/rcases.lean

added def tactic.merge_list

deleted def tactic.rcases_patt.name

deleted inductive tactic.rcases_patt