The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

I made my first tries in using Classes and Equivalences (Setoids, maybe). It can be seen at the same GitHub repository in the file matrices.v.
But I have hole in the vect_fold_Proper, which I have made Admitted. Can anyone help to fill it, please?

Also, is there any hints how to use such Setoids more effectively or idiomatic?

(I'm already trying first advanced rewrites, but they're not yet on Github.)

On Tue, Nov 5, 2013 at 11:24 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

Thanks to all for great hints. :) (And apologies for late answer.)

So I removed nz_type and made fin as this Definition fin l := {n | n <= l}, ignoring the idea of empty vectors.
Also I proved that Theorem fin_t1 {l} (n m: fin l): n = m <-> projT1 n = projT1 m. It made everything much easier (thanks to Cedric Auger).