The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

​Sorry, I was too fast in telling that "fin n" should be replaced with "vector unit n".

What I thought was redefining "fin n" with:

Fixpoint fin (n : nat) : Type :=

  match n with O => Empty_set | S n => option (fin n) end.

"vector unit n" is isomorphic to "unit", thus it would have been plain stupid to replace "fin n" with it.​

--

.../Sedrikov\...