Mathlib v3 is deprecated. Go to Mathlib v4

Inductive tactic.rcases_patt

Modification history

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