Induction nonsense
Ok this is a screenshot of this paper (end of p. 3) and it's the typing rule for the eliminator famInd
and its reduction rule
The indices of the recursive arguments \vec{v} are \vec{r}_i for each v_i
I don't see \vec{r}_i itself on the LHS of the reduction rule so I think you really need typed reduction to reduce the eliminator
re: t y p e s
I have it... the eliminator... at last...
But not for nested inductive types. I honestly don't know how to do that one and it seems like no one talks about them
Jon(athan)? | ionchy [jɑːnt͡ʃi] 🏳️🌈
MSc student in CS doing PL things 🇨🇦
@ionathanch on most places 🐦
PoGo: 8336 6654 0984
#WaterDrinker 💧
I have been blessed with admin powers on this instance and I will do my best not to muck things up
pfp: https://picrew.me/share?cd=6rKy0AQ4I3
header: https://doi.org/10.1145/2578855.2537850