Re: [mizar] strict

[Grzegorz Bancerek <bancerek@math.uwb.edu.pl>]

Quoting Adam Naumowicz <adamn@math.uwb.edu.pl>:

> "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.

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.
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 structure,
so, you must be careful to follow the order of structure widening in 
notations'
directive.

Grzegorz