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: adamn@mizar.org 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