Mathlib v3 is deprecated. Go to Mathlib v4

Def tactic.merge_list

Modification history

2018-08-08 06:57

tactic/rcases.lean

feat(tactic/rcases): rcases_hint, rintro_hint

Added tactic.merge_list View on Github →