Re: [mizar] widening BinOp to Relation

[Jesse Alama <alama@stanford.edu>]

Hi Adam,

Adam Naumowicz <adamn@math.uwb.edu.pl> writes:

> On Thu, 1 Feb 2007, Jesse Alama wrote:
>
>> 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?
>
> It seems that you don't have RELSET_1 present among your registrations
> directives. Tracing back the widening relation of BinOp of A one comes
> to Subset of [:A,A:] which is Relation-like only in the presence of a
> suitable registration from RELSET_1 - the first one.
>
> Please let me know if this solved the problem.

You were right -- including RELSET_1 in the registrations directive
solved the problem.  How did you know to look at RELSET_1?

Thanks much,

Jesse

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