Mathlib v3 is deprecated. Go to Mathlib v4

Structure tactic.interactive.rcases_config

Modification history

2018-08-08 14:39
tactic/interactive.lean
refactor(tactic/interactive): merge rcases_hint -> rcases?
Deleted tactic.interactive.rcases_configView on Github →
2018-08-08 06:57
tactic/interactive.lean
feat(tactic/rcases): rcases_hint, rintro_hint
Added tactic.interactive.rcases_configView on Github →