Re: [mizar] weak types

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

Josef:

>It seems to me that in the implementation, one would just
>have to remember for such types, that "consider" cannot be
>used,

Also, you don't get anymore from "for x holds P[]" (where x
doesn't occur in P[]) that "P[]" itself has to hold.

>Or is there any deeper reason for avoiding them?

It would be surprising.  PVS and Coq and NuPRL all support
types that can be empty.

In PVS I think that you indicate non-emptyness of a type by
writing TYPE+.  So for Mizar there might be similar syntax to
indicate that a mode is "weak":

	definition let ...;
	  weak mode ... -> ... means
	  ...
        end;
	  
(So what about existential clusters? :-))

By the way: a "cheap" way to implement these "possibly empty
types" would be to have them internally be represented by a
predicate, and then before trying to run CHECKER replacing
them by those predicates.  So

	for x being Large_Cardinal_that_may_not_exist
	  holds ...
	
would be first transformed into

	for x being set st Large_Cardinal_that_may_not_exist x
	  holds ...

and then the old CHECKER would be correct (but maybe too weak?)

Freek