Re: Vocabulary name overloading

Cytowanie Jeffrey Madsen <[email protected]>:

> I came across a puzzling error in the following snippet of code:
>
> definition
>   let R be comRing;
>   let I be Subset of Quot(R);
>   attr I is invertible means
>   :Def1:
>   I * I" = rng NatHom Quot(R);
> end;
>
> definition
>   let R be comRing;
>   let I be Subset of R;
>   attr I is invertible means
>   :Def2:
>   (NatHom Quot(R)) .: I is invertible;
> end;
>
> now
>   let R be comRing;
>   let I be Subset of R;
>   assume I is invertible;
>   then (NatHom Quot(R)) .: I is invertible by Def2;
> ::>                                         *4
> end;
>
> (NatHom Quot(R) has type "Function of R, Quot(R)".)
>
> The error does not occur when I give the two definitions different names,
> but I'd like to use the same name for both. What's weird is there shouldn't
> be any conflict, because "Subset of R" does not widen to "Subset of
> Quot(R)" or vice versa. Can anyone see what I'm doing wrong?
>
> Thanks,
>
> Jeff

Dear Jeff,

because Quot(R) is also comRing Mizar takes "Subset of <comRing>". To forse
"Subset of Qout(<comRing>)" you must change the order of the definitions but
it means you must change also the way of definition:-(
So, I advise the use of two different symbols.

Regards,
Grzegorz