Anders Mörtberg
Results
132
comments of
Anders Mörtberg
In the future we also plan to remove some dependencies on `Data.FinData` as inductive families are poorly supported in Cubical Agda and it would be better to use `Data.Fin` throughout...
I have no clue why this was so complicated and I like the new simpler version. Maybe @aljungstrom knows more? (It could have had something to do with attempts to...