Mathlib v3 is deprecated. Go to Mathlib v4

Def tactic.rcases_patt.name

Modification history

2018-08-08 06:57
tactic/rcases.lean
feat(tactic/rcases): rcases_hint, rintro_hint
Deleted tactic.rcases_patt.nameView on Github →
2017-08-18 03:14
tactic/rcases.lean
feat(tactic/rcases): recursive cases (with patterns) …
Added tactic.rcases_patt.nameView on Github →