Elaborating Inductive Definitions and Course-of-Values Induction in Cedille

Christopher Jenkins, Colin McDonald, Aaron Stump

In the Calculus of Dependent Lambda Eliminations (CDLE), a pure Curry-style type theory, it is possible to generically λ-encode inductive datatypes which support course-of-values (…