Re: [mizar] widening BinOp to Relation

[Jesse Alama <alama@stanford.edu>]

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

> On Fri, 2 Feb 2007, Jesse Alama wrote:
>
>>> 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?
>
> Expanding the mode 'BinOp of A' we get 'Function of [:A,A:],A', which
> in turn expands to 'quasi_total PartFunc of [:A,A:],A', and this means
> 'Function-like Relation of [:A,A:],A' which is eventually redefined as
> Subset of [:[:A,A:],A:]' in RELSET_1. The registration that follows
> this redefinition completes the job - providing the 'Relation-like'
> attribute:
>
> registration let X,Y;
>  cluster -> Relation-like Subset of [:X,Y:];
> end;

I follow the reason why my problem is solved given your hint to look
into RELSET_1.  But how did you know that RELSET_1 contained the key
to the solution?  Does this come from your knowledge of the MML?  An
MML query?  A mizar-mode command?

Jesse

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