[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Vocabulary name overloading

Cytowanie Jeffrey Madsen <jmadsen@nd.edu>:


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