[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] widening BinOp to Relation
Hi Jesse,
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.
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/
======================================================================