[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] strict
Quoting Grzegorz Bancerek <bancerek@math.uwb.edu.pl>:
Actually,
definition
let a1 be doubleLoopStr;
attr a1 is strict means
a1 = doubleLoopStr(#
the carrier of a1,
the add of a1,
the mult of a1,
the unity of a1,
the Zero of a1
#);
end;
The definition is generated and linked automatically by verifier when
necessary.
I.e., for each occurrence of "strict" attribute
So, no trace of the definition in Mizar XML files.
I think I better give full definition of strict attributes on MML
Query pages.
Attribute "strict" is defined and overloaded for each definition of
^^^^^^^
The better word is "declared".
structure,
so, you must be careful to follow the order of structure widening in
notations'
directive.
E.g., STRUCT_0 must be placed before RLVECT_1 and this before VECTSP_1
as ZeroStr <- LoopStr <- doubleLoopStr
Grzegorz