[mizar] widening BinOp to Relation

[Jesse Alama <alama@stanford.edu>]

I'm puzzled about the relation between BinOp and Relation.  I became
curious when I got the error

definition let p be polyhedron;
  func 0-circuit-sum(p) -> BinOp of 0-circuits(p) equals
  0-chain-sum(p)||0-circuits(p);
::>              *103

This error puzzled me because 0-chain-sum(p) is defined to have type
BinOp of 0-chains(p), and the functor || requires its left argument to
have Relation, and I assumed that the type BinOp widened to Relation.
I became even more puzzled when I looked at the statement of
REALSET1:3:

for X being set,
    F being BinOp of X,
    A being Preserv of F holds F||A is BinOp of A

As far as I can see, this statement ought to be flagged with error 103
for the same reason that my statement was flagged with that error.  No
new definition of BinOp is being used in REALSET1:3, as I confirmed by
browsing the semantic presentation of that article.

What might be going on?  Why would I get *103'd but not REALSET1:3?

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*56: Disagreement of types (http://www.mizar.org)