On Fri, 2 Feb 2007, Jesse Alama wrote:
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?
I must admit that my knowledge of MML alone wouldn't suffice to figure this out - I used the "View symbol def" feature for browsing in abstracts in Emacs - some knowledge of MML helped to speed up the search for the right occurrence of the symbols in question, though.
Best, Adam Naumowicz ====================================================================== Department of Applied Logic fax. +48 (85) 745-7662 Institute of Computer Science tel. +48 (85) 745-7559 (office) University of Bialystok e-mail: adamn@mizar.org Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/ ======================================================================