search

RedPRL / redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Apache License 2.0
204 stars 12 forks source link

Decompose elim into rec and case #454

Open jonsterling opened 5 years ago

jonsterling commented 5 years ago

@ecavallo I'd like to consider decomposing the eliminators into two different combinators: case and rec, as described in here: https://cs.ru.nl/~freek/courses/tt-2010/tvftl/epigram-notes.pdf

The idea is that case doesn't do any recursion, but just lets you see what constructor you have. And rec does the recursion (basically, for each type, it takes a motive P and provides all the recursive calls that can be made).

We'd have to make sure that this idea works for HITs, but a priori I have no reason to expect that it wouldn't extend directly.

Anyway, the benefit of this is that it separates the generation of the i.h. from the branching, and enables more flexible style of program, which will become important when we elaborate pattern matching.

ecavallo commented 5 years ago

I too see no reason why it wouldn't work. 👍

jonsterling commented 5 years ago

@ecavallo OK! We can investigate it later. I don't want to get distracted from finishing new-domain.