[mizar] What does this 'attr c1 is strict' convention mean?

[psvr <pmq2001@gmail.com>]

Hello everybody,

I've been reading through multiple mizar articles. When I encounter a struct definition, very frequently do I see

attr c₁ is strict ;

as the first line of the definition block, and then used in the selector line

       sel addF c₁ -> BinOp of the carrier of c₁;

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