Re: [mizar] weak types

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

Dear Andrzej,

>So the difference seems to be in the fact, that you want to state the guard,
>if you just write
>      T is natural_transformation
>and in Mizar we need guard only when the definition is actually used. It is
>something like lazy evaluation.
>I believe it is the main argument for the permissiveness.

I see.  I still don't like it.  Talking about 1/0, it's
nonsense.  1/0 is not 0, it is not some unknown real number,
it is _illegal._

But the main theorem of my paper with Jan can be interpreted
as that this "laziness" in Mizar is harmless.  In Mizar you
can not prove more than when you require (like I would
prefer) that all intermediate steps have to satisfy their
domain conditions.  So it is a strong argument for
permissiveness, yes.

By the way, by now you all know my dislike of only non-empty
types because of "Element of".  But _if_ empty types are
forbidden, I think that "Element of X" should have had a
guard "X is non empty set".

Freek