Mathlib v3 is deprecated. Go to Mathlib v4

Def tactic.interactive.rcases_patt_inverted

Modification history

2018-08-08 06:57
tactic/interactive.lean
feat(tactic/rcases): rcases_hint, rintro_hint
Deleted tactic.interactive.rcases_patt_invertedView on Github →
2018-05-20 06:37
tactic/interactive.lean
fix(tactic/interactive): make rcases handle nested constructors correctly …
Added tactic.interactive.rcases_patt_invertedView on Github →