[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] strict
Hi,
On Tue, 9 Jan 2007, Jesse Alama wrote:
definition
func F2 -> doubleLoopStr equals
coherence;
end;
there doesn't seem to be a definition of what it means to be a strict
doubleLoopStr; moreover, when I browse
http://mmlquery.mizar.org/mmlquery/fillin.php?filledfilename=phparticle.mqt&argument=article+vectsp_1
I see that there appears to be something like a definition:
definition
let a1 be doubleLoopStr;
attr a1 is strict;
end;
but when I browse VECTSP_1.MIZ, I don't see any definition of strict
for doubleLoopStr's. What's going on? What does "strict" mean? How
can I prove that a doubleLoopStr is strict?
"strict" doesn't have its own definition as it is a special (in a way
"meta" attribute) - it means that a term which has a structure type
<Theta> has exactly the same selectors (fields) as introduced in the
definition of the type <Theta>, so in your case only the selectors of a
doubleLoopStr - any extension to that would break the "strictness". So you
may think of a vector space as of a group, but it's not a "strict" group.
You don't have to worry about proving "strictness" with your definition -
if you define your functor using an "aggregate" structure term
explicitely enumerating all selectors, like
doubleLoopStr(# {0,1}, add2, prod2, unit2, zero2 #),
then the "strict" attribute is added automatically. This is why the
definition of "strict" has a special meaning which is automatically
defined separately for all structures - and it is added to the XML
presentation even if it's not present in the actual miz/abs file.
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/
======================================================================