[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] puzzling errors
On Sun, 11 Mar 2007, Jesse Alama wrote:
In the article I'm working on, the formula
bounding-0-circuit-space(p) is Subspace of 0-circuit-space(p)
is flagged with *101 ("Unknown mode") underneath the use of Subspace.
At the stage where this formula occurs in my article, the term
bounding-0-circuit-space is just a VectSpStr over F2 (the field {0,1}
with the usual operations). I'm trying to establish that it has type
VectSp of F2 by proving and then appealing to
for G being Field,
U being VectSp of G,
X being non empty Subset of the carrier of U,
f being BinOp of X,
l being Function of [:the carrier of G,X:],X,
z being Element of X
st f = (the add of U)||X &
l = (the lmult of U)|[:the carrier of G,X:] &
z = the Zero of U
holds VectSpStr (# X, f, z, l #) is Subspace of U;
What surprises me is that this formula is flagged only with *4; it is
not flagged with *101. That suggests that the last formula
VectSpStr (# X, f, z, l #) is Subspace of U
is well-formed (in the sense that the use of Subspace there isn't
flagged with *101). Why is my theorem about Subspaces not flagged
with *101 but my claim about bounding-0-circuit-space(p) is flagged
with that error?
I guess the term '0-circuit-space(p)' is the culprit here - it seems its
type doesn't widen to 'Vectsp of F', where F is some field.
In geeral, one can always 'qualify'
<term> is <type>;
any term with any valid type, and depending on if this is true or not,
only the error *4 is reported.
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/
======================================================================