Syntax

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Attributes had been introduced as syntactic sugar, but they become now
more and more important feature of the Mizar language. Still, many
decisions are postponed, it is time to do something about this.

When attributes had been implemented, we revised the library, replacing
some modes and predicates by attributes.

A mode might be changed to an attribute if all loci are available from its
mother type, and a predicate, if it has one visible argument. (some of you
know what I mean, some are not really interested; if anybody wants
explanations, please write).

In the process, we must find symbols for attributes.  We used
       M-like
where M stands for a mode symbol. In the case of predicates it was more
complicated. If the predicate symbol is of the form
      is_...
then the attribute is
      being_...

Then instead of 
  R is_quasi_order   (ORDERS_1:def 1)
one could write
  R is being_quasi_order

Similarly for
  F has_a_unity       (SETWISEO:def 2)
one can write
  F is having_a_unity  

We hoped that it is a temporary solution, of course. And if we found
something nicer then it is used. E.g
for

  C has_finite_products  (CAT_4:def 3)
we introduced
  C is with_finite_products  (not "C is having_finite_products")

or for

 F is_collinear   (INCSP_1:def 6)

 F is linear   (not "F is being_collinear")

Still, to have nicer notation, we allow, as yet, for Predicate Synonyms.
We propose to to simplify the grammar and to eliminate them. Maybe there
are cases when it would be better to keep them, e.g.

the synonym
    |-  f     (CQC_THE1:def 10)
     
for
     f is valid,

but the gain is not sufficiently big. 

We have now of course to change the attribute symbols. For
"having_...", "with_..." seems to be good, for other "continuous" form we
have to find something.

If you can propose a reonable solution, both for general case and for a
particular attribute, please write to mizar-forum.

Regards,
Andrzej

Andrzej Trybulec
Institute of Computer Science
University of Bialystok
ul. Akademicka 2
Bialystok, Poland