Re: [mizar] Once more: empty types

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

On Wed, Nov 07, 2007 at 05:09:46PM +0100, Freek Wiedijk wrote:

> So I wondered whether there was anyone
> beyond you and me...  For instance, what does Piotr think
> of this, I wonder.  Does he also think it's not a big deal?

I have not participated in the discussion before and I will refrain
from doing so now.  I would like to make two remarks.

 - I have never run into a situtation when a possibly empty type would 
   make a formalization more natural.  The discussion from a year ago
   was inconclusive as I did not see answers to Andrzej's arguments how
   to work around possibly empty types.  

 - Changing anything in the Mizar verifier is a problem since there
   are so few people that can modify the code (I am not one of them). 
   These people are usually very busy and do not have time for experimenting
   with ideas for which there is no general concensus.  The effort
   of implementing possibly empty types can be estimated only by attempting
   to implement the feature.  Who will do it?

Cheers, 

PR

-- 
Piotr Rudnicki                                http://web.cs.ualberta.ca/~piotr