Re: [mizar] Why do Mizar types have to be non-empty?

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Andrzej,

>The main reason is that in CHECKER fictitious variables
>(that not occur in the scope) are not instantiated. If types
>may be empty, we have to instatiate them.

I do not understand, sorry.  Can you give an example?

>Also it is nice, that if I need an arbitrary object of
>type \theta, I can write
>     consider x being \theta;
>(it happens quite often) and I do not look for a justification.

In a "Mizar with empty types" you could still have
existential clusters for this purpose.  You could then have
the "empty cluster" for \theta, to be allowed to say this.
So that doesn't seem a reason _not_ to allow empty types.

Freek