Re: Zero or empty set

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

Piotr Rudnicki wrote:
> 
> How about promoting all numerals to functors?
> 
> With this one would be able to register clusters for them and some of
> them are quite useful, eg.  2 -> even.
> 

It might be a good idea, however is is now rather difficult to
anticipate the effects of any, more substantial, change in Mizar.
So I would like start with 0 and see what will happen.

Should we allow for registration like

   cluster 2*n -> even;
It is now allowed?

Then may be it woulde be better, if Mizar knew that 2 is of the form
2*1?

On the aother hand if numerals are just functors, we have no way to
treat them uniformely (any functor by itself).

As you see I have no opinion.

Andrzej