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

[Andrzej Trybulec <trybulec@cs.shinshu-u.ac.jp>]

Freek Wiedijk wrote:

> >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.

In a bit older Mizar (8 years ago?) we had two kinds of attribute
definitions:

    attr attr_symbol -> the_type_of_the_subject means
    mode attr_symbol -> the_type_of_the_subject means

In the second version the 'existence' condition was obligatory. It must
be now registered as a cluster. Only the first version is used, with
quite a different syntax, previously the subject was not listed among
the loci, but called 'it'. So, as you see, in this case what you propose
is already done.

BTW. Are you sure that your 'normal form' is a type, not an attribute?

Andrzej