KnownNat-indexed vectors

mixphix:

Are there Num instances for any of these Finite types?

Is the product of two rings a ring? If not, there should not be such an instance in general. Finite n can be a field if n is prime, if I am not mistaken. But why would you want a Num instance on the index set anyways?

mixphix:

This approach has the advantage that it doesn’t “segfault” if indexing past the length

If you are not striving for type-safe indexing, why pursue this approach at all?

I forgot to mention Henning Thielemann’s linear algebra ecosystem with lapack, comfort-array and its shapes.