The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jeff,

I wonder what is the advantage of using a definition of Fin n which is 
equivalent to False for n=0 in connection with Vectors which exist for n=0. 
What bad things would happen if Fin 0 would be defined and equivalent to a 
0-tuple of unit rather than something which doesn't exist at all? Is the fact 
that Fin 0 -> False used for ex falso quod libet proofs in some places? Since 
the 0 length constructor of vectors is trivial I don't see many applications 
for this. So unless you really need ex falso quod libet proofs using Fin 0 
somewhere, I have doubts that this is the most efficient (in terms of human 
time to get things done) way of setting up things.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928