Custom Representations of Inductive Families

Constantine Theocharis, Edwin Brady

Inductive families provide a convenient way of programming with dependent types. Yet, when it comes to compilation, their default linked-tree runtime representations, as well as th…