Re: What does this 'attr c1 is strict' convention mean?

Dear P.S.V.R,

The definitions of the attributes "strict" that you can find in the 
HTML-ized presentation of Mizar articles represent special attributes 
automatically generated for any newly introduced structure (that's why 
one doesn't see them in the normal Mizar text, i.e. the *.miz files).
For a given structure type its "strict" attribute means that an object 
with this property is a structure whose set of selectors (fields) is 
exactly the same as in the definition of the structural type. E.g. any 
TopStruct with a carrier and topology is also a 1-sorted, but it is not a 
strict 1-sorted because of the extra topology. So the "strictness" is a 
technical property and as such it doesn't require any definition. But for 
the sake of full linking in the HTML presentation it is visible there, 
with the c-thing being the local constant representing the notion being 
defined in a given definition (again a technical thing).

Best regards,

Adam Naumowicz

=======================================================================
Dept. of Programming and Formal Methods  Fax: +48(85)7457662
Institute of Informatics                 Tel: +48(85)7457559 (office)
University of Bialystok                  E-mail: [email protected]
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================

On Wed, 5 Oct 2011, psvr wrote:

> Hello everybody,
>
> I've been reading through multiple mizar articles. When I encounter a struct definition, very frequently do I see
> 	attr c1 is strict ;
> as the first line of the definition block, and then used in the selector line
>       sel addF c1 -> BinOp of the carrier of c1;
> Does this mean "carrier of strict"? I'm confused to see that "strict" appears after the word "of". What does this mean?
>
> This seems to be a convention, and I cannot understand why should it declare this c_1 thing. Seeing it being named c_1, is there any circumstances that more c_2, c_3, etc are needed?
>
> Thank you very much.
>
> P.S.V.R
>