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

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

Dear Andrzej,

>You may use a permissive definition, say
>
>definition let R be redunction-relation such that
>Z:  R has_normal_forms;
>  mode Normal_form of R means
>   it is_normal_form;
>  existence by Z;
>end;

I didn't know you could have "assume" in a mode definition
too!

So what is the meaning of "n is Normal_form of R" when this
"Z" condition fails?  Is it an "unknown" statement, just like
sqrt(-1) is an "unknown real number" (where I mean the "sqrt"
from SQUARE_1:def 4).  Or is it just equivalent to
"contradiction"? (which seems appropriate in this case, if R
doesn't have normal forms, then n should not have type
"normal form" :-))

Freek