[mizar] Type extensions

[Adam Grabowski <adam@math.uwb.edu.pl>]

  Dear all,
  in one of the articles recently submitted to the Mizar Mathematical
Library (currently under review process) one can find the following
definition:

definition
  let X be non empty set;
  let S be SigmaField of X;
  let M be sigma_Measure of S;
  let f be PartFunc of X,REAL;
  func Integral(M,f) -> Element of ExtREAL equals
    Integral(M,R_EAL f);
  coherence;
end;

where "Integral" was defined in MESFUNC5 for "f" of the type
PartFunc of X, ExtREAL (the remaining variables are of the same
type as in the above definition). Even if the set "REAL" (the set of
all real numbers) is a subset of "ExtREAL" (the set extending REAL
by the infinite values), the Mizar system does not give automatically
a type "PartFunc of X,ExtREAL" to partial functions of X, REAL.
This could result in the duplication of notions, even if only some
casting functions are used instead of defining notions from scratch.
(as R_EAL f just assigns the type "PartFunc of X, ExtREAL" to f which
is a partial function from X into REAL).

Very similar problem apeared in the case of the type "Element of REAL"
and "Element of COMPLEX" (with the earlier not extending to the latter).
Now we force the users to use "real number" and "complex number",
respectively. Thanks to the mechanism of the conditional clusters
with the registration as follows:

definition
  cluster real -> complex number;
  coherence; :: with some easy proof to be found in XREAL_0
end;

a number of duplications can be avoided.

I would like to know your opinion about the best solution
(or at least, the better one) in the case of partial functions
(and hopefully, some general guidelines for the future).
  Regards,
  Adam Grabowski
  Library Committee of the Association of Mizar Users