|
|
Abstract:
Coquand[1] has shown that pattern matching in the presence of dependent types and inductive families introduces a new dimension not present in the non-dependent case, such as the possibility of non-linear patterns and elimination of empty cases. More recently, these mechanisms have been implemented in programming languages with dependent types such as Agda[2] and Epigram[3]. We propose a new elimination rule for Coq that adapts some of those ideas. Through a series of examples, we will show some advantages over the current elimination rule, and the practical and theoretical consequences of our proposal.
[1] T. Coquand. Pattern Matching with Dependent Types, 1992.
|