[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