Re: [mizar] clusters of predicates

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

One similar idea on the automation, now about functors:

We have TOP-REAL n defined in  EUCLID:def 8 via "equals" as
TopSpaceMetr (Euclid n);

This is a serious pain when dependent type occurs:

Subset of TOP-REAL n is now not identified with 
Subset of TopSpaceMetr (Euclid n) .

We could allow more general notion of synonyms, i.e.
synonym TOP-REAL n for TopSpaceMetr (Euclid n) which would solve this. 
This is probably the easiest solution, but on the other hand, TOP-REAL 
seems important enough to "exist" on the object level, not just as a 
macro.

So other solution is to allow the definitions via "equals" to construct a 
hierarchy of terms. There are already now plans to use this infprmation in 
the checker, however we would need to use this hierarchy also during 
identification (analyzer).

In case such mechanism is too strong and sometimes unwanted ( I do not 
know), we could have a special keyword, e.g. st. like

func TOP-REAL n instantiates TopSpaceMetr (Euclid n);

Josef